1 /-
2 Copyright (c) 2015 Microsoft Corporation. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Leonardo de Moura, Mario Carneiro
5
6 In the standard library we cannot assume the univalence axiom.
7 We say two types are equivalent if they are isomorphic.
8
9 Two equivalent types have the same cardinality.
10 -/
11 import tactic.split_ifs logic.function logic.unique data.set.function data.bool data.quot
src └──────────────┘ └────────────┘ └──────────┘ └───────────────┘ └───────┘ └───────┘
12
13 open function
14
15 universes u v w
16 variables {α : Sort u} {β : Sort v} {γ : Sort w}
17
18 /-- `α ≃ β` is the type of functions from `α → β` with a two-sided inverse. -/
19 structure equiv (α : Sort*) (β : Sort*) :=
id └───┘ └───┘
typ └───┘ └───┘
20 (to_fun : α → β)
id ┴ ┴ ┴
typ ┴ ┴ ┴
21 (inv_fun : β → α)
id ┴ ┴ ┴
typ ┴ ┴ ┴
22 (left_inv : left_inverse inv_fun to_fun)
id └──────────┘ └─────┘ └────┘
src └──────────┘
typ └──────────┘ └─────┘ └────┘
23 (right_inv : right_inverse inv_fun to_fun)
id └───────────┘ └─────┘ └────┘
src └───────────┘
typ └───────────┘ └─────┘ └────┘
24
25 infix ` ≃ `:25 := equiv
id └───┘
src └───┘
typ └───┘
doc └───┘
26
27 def function.involutive.to_equiv {f : α → α} (h : involutive f) : α ≃ α :=
id ┴ ┴ └────────┘ ┴ ┴ ┴ ┴
src └────────┘ ┴
typ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴
doc └────────┘ ┴
28 ⟨f, f, h.left_inverse, h.right_inverse⟩
id ┴ ┴ ┴└───────────┘ ┴└────────────┘
src └───────────┘ └────────────┘
typ ┴ ┴ ┴└───────────┘ ┴└────────────┘
29
30 namespace equiv
31
32 /-- `perm α` is the type of bijections from `α` to itself. -/
33 @[reducible] def perm (α : Sort*) := equiv α α
id └───┘ ┴ ┴
src └───┘
typ └───┘ ┴ ┴
doc └───────┘ └───┘
34
35 instance : has_coe_to_fun (α ≃ β) :=
id └────────────┘ ┴ ┴ ┴
src └────────────┘ ┴
typ └────────────┘ ┴ ┴ ┴
doc ┴
36 ⟨_, to_fun⟩
id └────┘
src └────┘
typ └────┘
37
38 @[simp] theorem coe_fn_mk (f : α → β) (g l r) : (equiv.mk f g l r : α → β) = f :=
id ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴
typ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
39 rfl
id └─┘
src └─┘
typ └─┘
40
41 theorem eq_of_to_fun_eq : ∀ {e₁ e₂ : equiv α β}, (e₁ : α → β) = e₂ → e₁ = e₂
id ┴ └───┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └┘ ┴ └┘
src └───┘ ┴ ┴
typ ┴ └───┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └┘ ┴ └┘
doc └───┘
42 | ⟨f₁, g₁, l₁, r₁⟩ ⟨f₂, g₂, l₂, r₂⟩ h :=
id └┘ └┘ └┘ └┘ └┘ └┘ └┘ ┴
typ └┘ └┘ └┘ └┘ └┘ └┘ └┘ ┴
43 have f₁ = f₂, from h,
id ┴
src ┴
typ ┴
44 have g₁ = g₂, from funext $ assume x,
id ┴ └────┘ ┴
src ┴ └────┘
typ ┴ └────┘ ┴
45 have f₁ (g₁ x) = f₂ (g₂ x), from (r₁ x).trans (r₂ x).symm,
id ┴ ┴ ┴ ┴ └───┘ ┴ └──┘
src ┴ └───┘ └──┘
typ ┴ ┴ ┴ ┴ └───┘ ┴ └──┘
46 have f₁ (g₁ x) = f₁ (g₂ x), by { subst f₂, exact this },
id ┴ ┴ ┴ └┘ └──┘
src ┴ └────┘ └────┘ ┴
typ ┴ ┴ ┴ └────┘└┘ └────┘└──┘┴
doc └────┘ └────┘ ┴
txt └────┘ └────┘ ┴
par └────┘ └────┘ ┴
pid ┴ ┴ ┴
st └─────────┘└───────────┘└┘
47 show g₁ x = g₂ x, from injective_of_left_inverse l₁ this,
id ┴ ┴ ┴ └───────────────────────┘ └──┘
src ┴ └───────────────────────┘
typ ┴ ┴ ┴ └───────────────────────┘ └──┘
48 by simp *
src └──────
typ └──────
doc └──────
txt └──────
par └──────
pid ┴┴└
st └───────
49
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
50 @[ext] lemma ext (f g : equiv α β) (H : ∀ x, f x = g x) : f = g :=
id └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─┘ └───┘
51 eq_of_to_fun_eq (funext H)
id └─────────────┘ └────┘ ┴
src └─────────────┘ └────┘
typ └─────────────┘ └────┘ ┴
52
53 @[ext] lemma perm.ext (σ τ : equiv.perm α) (H : ∀ x, σ x = τ x) : σ = τ :=
id └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ ┴ ┴
typ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─┘ └────────┘
54 equiv.ext _ _ H
id └───────┘ ┴
src └───────┘
typ └───────┘ ┴
55
56 @[refl] protected def refl (α : Sort*) : α ≃ α := ⟨id, id, λ x, rfl, λ x, rfl⟩
id ┴ ┴ ┴ └┘ └┘ ┴ └─┘ ┴ └─┘
src └──┘ ┴ └┘ └┘ └─┘ └─┘
typ ┴ ┴ ┴ └┘ └┘ ┴ └─┘ ┴ └─┘
doc └──┘ ┴
57
58 @[symm] protected def symm (e : α ≃ β) : β ≃ α := ⟨e.inv_fun, e.to_fun, e.right_inv, e.left_inv⟩
id ┴ ┴ ┴ ┴ ┴ ┴ ┴└──────┘ ┴└─────┘ ┴└────────┘ ┴└───────┘
src └──┘ ┴ ┴ └──────┘ └─────┘ └────────┘ └───────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴└──────┘ ┴└─────┘ ┴└────────┘ ┴└───────┘
doc └──┘ ┴ ┴
59
60 @[trans] protected def trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘ ┴ ┴ ┴
61 ⟨e₂.to_fun ∘ e₁.to_fun, e₁.inv_fun ∘ e₂.inv_fun,
id └┘└─────┘ ┴ └┘└─────┘ └┘└──────┘ ┴ └┘└──────┘
src └─────┘ ┴ └─────┘ └──────┘ ┴ └──────┘
typ └┘└─────┘ ┴ └┘└─────┘ └┘└──────┘ ┴ └┘└──────┘
62 e₂.left_inv.comp e₁.left_inv, e₂.right_inv.comp e₁.right_inv⟩
id └┘└───────┘└───┘ └┘└───────┘ └┘└────────┘└───┘ └┘└────────┘
src └───────┘└───┘ └───────┘ └────────┘└───┘ └────────┘
typ └┘└───────┘└───┘ └┘└───────┘ └┘└────────┘└───┘ └┘└────────┘
63
64 protected theorem injective : ∀ f : α ≃ β, injective f
id ┴ ┴ ┴ ┴ └───────┘ ┴
src ┴ └───────┘
typ ┴ ┴ ┴ ┴ └───────┘ ┴
doc ┴
65 | ⟨f, g, h₁, h₂⟩ := injective_of_left_inverse h₁
id └┘ └───────────────────────┘
src └───────────────────────┘
typ └┘ └───────────────────────┘
66
67 protected theorem surjective : ∀ f : α ≃ β, surjective f
id ┴ ┴ ┴ ┴ └────────┘ ┴
src ┴ └────────┘
typ ┴ ┴ ┴ ┴ └────────┘ ┴
doc ┴
68 | ⟨f, g, h₁, h₂⟩ := surjective_of_has_right_inverse ⟨_, h₂⟩
id └┘ └─────────────────────────────┘
src └─────────────────────────────┘
typ └┘ └─────────────────────────────┘
69
70 protected theorem bijective (f : α ≃ β) : bijective f :=
id ┴ ┴ ┴ └───────┘ ┴
src ┴ └───────┘
typ ┴ ┴ ┴ └───────┘ ┴
doc ┴
71 ⟨f.injective, f.surjective⟩
id ┴└────────┘ ┴└─────────┘
src └────────┘ └─────────┘
typ ┴└────────┘ ┴└─────────┘
72
73 @[simp] lemma range_eq_univ {α : Type*} {β : Type*} (e : α ≃ β) : set.range e = set.univ :=
id ┴ ┴ ┴ └───────┘ ┴ ┴ └──────┘
src ┴ └───────┘ ┴ └──────┘
typ ┴ ┴ ┴ └───────┘ ┴ ┴ └──────┘
doc └──┘ ┴ └───────┘
74 set.eq_univ_of_forall e.surjective
id └───────────────────┘ ┴└─────────┘
src └───────────────────┘ └─────────┘
typ └───────────────────┘ ┴└─────────┘
75
76 protected theorem subsingleton (e : α ≃ β) : ∀ [subsingleton β], subsingleton α
id ┴ ┴ ┴ └───────────┘ ┴ └──────────┘ ┴
src ┴ └───────────┘ └──────────┘
typ ┴ ┴ ┴ ┴└──────────┘ ┴ └──────────┘ ┴
doc ┴
77 | ⟨H⟩ := ⟨λ a b, e.injective (H _ _)⟩
id ┴ ┴ ┴ ┴└────────┘
src └────────┘
typ ┴ ┴ ┴ ┴└────────┘
78
79 protected def decidable_eq (e : α ≃ β) [H : decidable_eq β] : decidable_eq α
id ┴ ┴ ┴ └──────────┘ ┴ └──────────┘ ┴
src ┴ └──────────┘ └──────────┘
typ ┴ ┴ ┴ └──────────┘ ┴ └──────────┘ ┴
doc ┴
80 | a b := decidable_of_iff _ e.injective.eq_iff
id └──────────────┘ ┴└────────┘└─────┘
src └──────────────┘ └────────┘└─────┘
typ └──────────────┘ ┴└────────┘└─────┘
81
82 lemma nonempty_iff_nonempty : α ≃ β → (nonempty α ↔ nonempty β)
id ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴
src ┴ └──────┘ ┴ └──────┘
typ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴
doc ┴
83 | ⟨f, g, _, _⟩ := nonempty.congr f g
id ┴ ┴ └────────────┘
src └────────────┘
typ ┴ ┴ └────────────┘
84
85 protected def cast {α β : Sort*} (h : α = β) : α ≃ β :=
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
86 ⟨cast h, cast h.symm, λ x, by { cases h, refl }, λ x, by { cases h, refl }⟩
id └──┘ ┴ └──┘ ┴└───┘ ┴ ┴ ┴ ┴
src └──┘ └──┘ └───┘ └────┘ └───┘ └────┘ └───┘
typ └──┘ ┴ └──┘ ┴└───┘ ┴ └────┘┴ └───┘ ┴ └────┘┴ └───┘
doc └────┘ └───┘ └────┘ └───┘
txt └────┘ └───┘ └────┘ └───┘
par └────┘ └───┘ └────┘ └───┘
pid ┴ ┴ ┴ ┴
st └────────┘└─────┘└┘ └────────┘└─────┘└┘
87
88 @[simp] theorem coe_fn_symm_mk (f : α → β) (g l r) : ((equiv.mk f g l r).symm : β → α) = g :=
id ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
src └──────┘ └──┘ ┴
typ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
doc └──┘
89 rfl
id └─┘
src └─┘
typ └─┘
90
91 @[simp] theorem refl_apply (x : α) : equiv.refl α x = x := rfl
id ┴ └────────┘ ┴ ┴ ┴ ┴ └─┘
src └────────┘ ┴ └─┘
typ ┴ └────────┘ ┴ ┴ ┴ ┴ └─┘
doc └──┘
92
93 @[simp] theorem trans_apply (f : α ≃ β) (g : β ≃ γ) (a : α) : (f.trans g) a = g (f a) := rfl
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
src ┴ ┴ └────┘ ┴ └─┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
doc └──┘ ┴ ┴
94
95 @[simp] theorem apply_symm_apply : ∀ (e : α ≃ β) (x : β), e (e.symm x) = x
id ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴
src ┴ └───┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴
doc └──┘ ┴
96 | ⟨f₁, g₁, l₁, r₁⟩ x := by { simp [equiv.symm], rw r₁ }
id └┘ └────────┘ └┘
src └────┘└────────┘┴ └─┘ ┴
typ └┘ └────┘└────────┘┴ └─┘└┘┴
doc └────┘ ┴ └─┘ ┴
txt └────┘ ┴ └─┘ ┴
par └────┘ ┴ └─┘ ┴
pid ┴┴ ┴ ┴ ┴
st └──────────────────┘└──────┘└┘
97
98 @[simp] theorem symm_apply_apply : ∀ (e : α ≃ β) (x : α), e.symm (e x) = x
id ┴ ┴ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴
src ┴ └───┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴
doc └──┘ ┴
99 | ⟨f₁, g₁, l₁, r₁⟩ x := by { simp [equiv.symm], rw l₁ }
id └┘ └────────┘ └┘
src └────┘└────────┘┴ └─┘ ┴
typ └┘ └────┘└────────┘┴ └─┘└┘┴
doc └────┘ ┴ └─┘ ┴
txt └────┘ ┴ └─┘ ┴
par └────┘ ┴ └─┘ ┴
pid ┴┴ ┴ ┴ ┴
st └──────────────────┘└──────┘└┘
100
101 @[simp] lemma symm_trans_apply (f : α ≃ β) (g : β ≃ γ) (a : γ) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ ┴ ┴
102 (f.trans g).symm a = f.symm (g.symm a) := rfl
id ┴└────┘ ┴ └──┘ ┴ ┴ ┴└───┘ ┴└───┘ ┴ └─┘
src └────┘ └──┘ ┴ └───┘ └───┘ └─┘
typ ┴└────┘ ┴ └──┘ ┴ ┴ ┴└───┘ ┴└───┘ ┴ └─┘
103
104 @[simp] theorem apply_eq_iff_eq : ∀ (f : α ≃ β) (x y : α), f x = f y ↔ x = y
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ ┴
105 | ⟨f₁, g₁, l₁, r₁⟩ x y := (injective_of_left_inverse l₁).eq_iff
id └┘ └───────────────────────┘ └────┘
src └───────────────────────┘ └────┘
typ └┘ └───────────────────────┘ └────┘
106
107 @[simp] theorem cast_apply {α β} (h : α = β) (x : α) : equiv.cast h x = cast h x := rfl
id ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ └──┘ ┴ ┴ └─┘
src ┴ └────────┘ ┴ └──┘ └─┘
typ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ └──┘ ┴ ┴ └─┘
doc └──┘
108
109 lemma symm_apply_eq {α β} (e : α ≃ β) {x y} : e.symm x = y ↔ x = e y :=
id ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └───┘ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
110 ⟨λ H, by simp [H.symm], λ H, by simp [H]⟩
id ┴ ┴ ┴
src └────┘ ┴ └────┘ ┴
typ ┴ └────┘└────┘┴ ┴ └────┘┴┴
doc └────┘ ┴ └────┘ ┴
txt └────┘ ┴ └────┘ ┴
par └────┘ ┴ └────┘ ┴
pid ┴┴ ┴ ┴┴ ┴
st └────────────┘ └───────┘
111
112 lemma eq_symm_apply {α β} (e : α ≃ β) {x y} : y = e.symm x ↔ e y = x :=
id ┴ ┴ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └───┘ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
113 (eq_comm.trans e.symm_apply_eq).trans eq_comm
id └─────┘└────┘ ┴└────────────┘ └───┘ └─────┘
src └─────┘└────┘ └────────────┘ └───┘ └─────┘
typ └─────┘└────┘ ┴└────────────┘ └───┘ └─────┘
114
115 @[simp] theorem symm_symm (e : α ≃ β) : e.symm.symm = e := by { cases e, refl }
id ┴ ┴ ┴ ┴└────────┘ ┴ ┴ ┴
src ┴ └────────┘ ┴ └────┘ └───┘
typ ┴ ┴ ┴ ┴└───┘└───┘ ┴ ┴ └────┘┴ └───┘
doc └──┘ ┴ └────┘ └───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴ ┴
st └────────┘└─────┘└┘
116
117 @[simp] theorem symm_symm_apply (e : α ≃ β) (a : α) : e.symm.symm a = e a := by { cases e, refl }
id ┴ ┴ ┴ ┴ ┴└────────┘ ┴ ┴ ┴ ┴ ┴
src ┴ └────────┘ ┴ └────┘ └───┘
typ ┴ ┴ ┴ ┴ ┴└───┘└───┘ ┴ ┴ ┴ ┴ └────┘┴ └───┘
doc └──┘ ┴ └────┘ └───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴ ┴
st └────────┘└─────┘└┘
118
119 @[simp] theorem trans_refl (e : α ≃ β) : e.trans (equiv.refl β) = e := by { cases e, refl }
id ┴ ┴ ┴ ┴└────┘ └────────┘ ┴ ┴ ┴ ┴
src ┴ └────┘ └────────┘ ┴ └────┘ └───┘
typ ┴ ┴ ┴ ┴└────┘ └────────┘ ┴ ┴ ┴ └────┘┴ └───┘
doc └──┘ ┴ └────┘ └───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴ ┴
st └────────┘└─────┘└┘
120
121 @[simp] theorem refl_symm : (equiv.refl α).symm = equiv.refl α := rfl
id └────────┘ ┴ └──┘ ┴ └────────┘ ┴ └─┘
src └────────┘ └──┘ ┴ └────────┘ └─┘
typ └────────┘ ┴ └──┘ ┴ └────────┘ ┴ └─┘
doc └──┘
122
123 @[simp] theorem refl_trans (e : α ≃ β) : (equiv.refl α).trans e = e := by { cases e, refl }
id ┴ ┴ ┴ └────────┘ ┴ └───┘ ┴ ┴ ┴ ┴
src ┴ └────────┘ └───┘ ┴ └────┘ └───┘
typ ┴ ┴ ┴ └────────┘ ┴ └───┘ ┴ ┴ ┴ └────┘┴ └───┘
doc └──┘ ┴ └────┘ └───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴ ┴
st └────────┘└─────┘└┘
124
125 @[simp] theorem symm_trans (e : α ≃ β) : e.symm.trans e = equiv.refl β := ext _ _ (by simp)
id ┴ ┴ ┴ ┴└───┘└────┘ ┴ ┴ └────────┘ ┴ └─┘
src ┴ └───┘└────┘ ┴ └────────┘ └─┘ └──┘
typ ┴ ┴ ┴ ┴└───┘└────┘ ┴ ┴ └────────┘ ┴ └─┘ └──┘
doc └──┘ ┴ └──┘
txt └──┘
par └──┘
st └───┘
126
127 @[simp] theorem trans_symm (e : α ≃ β) : e.trans e.symm = equiv.refl α := ext _ _ (by simp)
id ┴ ┴ ┴ ┴└────┘ ┴└───┘ ┴ └────────┘ ┴ └─┘
src ┴ └────┘ └───┘ ┴ └────────┘ └─┘ └──┘
typ ┴ ┴ ┴ ┴└────┘ ┴└───┘ ┴ └────────┘ ┴ └─┘ └──┘
doc └──┘ ┴ └──┘
txt └──┘
par └──┘
st └───┘
128
129 lemma trans_assoc {δ} (ab : α ≃ β) (bc : β ≃ γ) (cd : γ ≃ δ) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴
130 (ab.trans bc).trans cd = ab.trans (bc.trans cd) :=
id └┘└────┘ └┘ └───┘ └┘ ┴ └┘└────┘ └┘└────┘ └┘
src └────┘ └───┘ ┴ └────┘ └────┘
typ └┘└────┘ └┘ └───┘ └┘ ┴ └┘└────┘ └┘└────┘ └┘
131 equiv.ext _ _ $ assume a, rfl
id └───────┘ ┴ └─┘
src └───────┘ └─┘
typ └───────┘ ┴ └─┘
132
133 theorem left_inverse_symm (f : equiv α β) : left_inverse f.symm f := f.left_inv
id └───┘ ┴ ┴ └──────────┘ ┴└───┘ ┴ ┴└───────┘
src └───┘ └──────────┘ └───┘ └───────┘
typ └───┘ ┴ ┴ └──────────┘ ┴└───┘ ┴ ┴└───────┘
doc └───┘
134
135 theorem right_inverse_symm (f : equiv α β) : function.right_inverse f.symm f := f.right_inv
id └───┘ ┴ ┴ └────────────────────┘ ┴└───┘ ┴ ┴└────────┘
src └───┘ └────────────────────┘ └───┘ └────────┘
typ └───┘ ┴ ┴ └────────────────────┘ ┴└───┘ ┴ ┴└────────┘
doc └───┘
136
137 def equiv_congr {δ} (ab : α ≃ β) (cd : γ ≃ δ) : (α ≃ γ) ≃ (β ≃ δ) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴ ┴
138 ⟨ λac, (ab.symm.trans ac).trans cd, λbd, ab.trans $ bd.trans $ cd.symm,
id └┘ └┘└───┘└────┘ └┘ └───┘ └┘ └┘ └┘└────┘ └┘└────┘ └┘└───┘
src └───┘└────┘ └───┘ └────┘ └────┘ └───┘
typ └┘ └┘└───┘└────┘ └┘ └───┘ └┘ └┘ └┘└────┘ └┘└────┘ └┘└───┘
139 assume ac, begin simp [trans_assoc], rw [← trans_assoc], simp end,
id └┘ └─────────┘ └─────────┘
src └────┘└─────────┘┴ └────┘└─────────┘┴ └───┘
typ └┘ └────┘└─────────┘┴ └────┘└─────────┘┴ └───┘
doc └────┘ ┴ └────┘ ┴ └───┘
txt └────┘ ┴ └────┘ ┴ └───┘
par └────┘ ┴ └────┘ ┴ └───┘
pid ┴┴ ┴ └──┘ ┴ ┴
st └──────────────────────┘└─────────────────┘└──────┘└─┘
140 assume ac, begin simp [trans_assoc], rw [← trans_assoc], simp end, ⟩
id └┘ └─────────┘ └─────────┘
src └────┘└─────────┘┴ └────┘└─────────┘┴ └───┘
typ └┘ └────┘└─────────┘┴ └────┘└─────────┘┴ └───┘
doc └────┘ ┴ └────┘ ┴ └───┘
txt └────┘ ┴ └────┘ ┴ └───┘
par └────┘ ┴ └────┘ ┴ └───┘
pid ┴┴ ┴ └──┘ ┴ ┴
st └──────────────────────┘└─────────────────┘└──────┘└─┘
141
142 def perm_congr {α : Type*} {β : Type*} (e : α ≃ β) : perm α ≃ perm β :=
id ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
src ┴ └──┘ ┴ └──┘
typ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
doc ┴ └──┘ ┴ └──┘
143 equiv_congr e e
id └─────────┘ ┴ ┴
src └─────────┘
typ └─────────┘ ┴ ┴
144
145 protected lemma image_eq_preimage {α β} (e : α ≃ β) (s : set α) : e '' s = e.symm ⁻¹' s :=
id ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴└───┘ └─┘ ┴
src ┴ └─┘ └┘ ┴ └───┘ └─┘
typ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴└───┘ └─┘ ┴
doc ┴ └─┘
146 set.ext $ assume x, set.mem_image_iff_of_inverse e.left_inv e.right_inv
id └─────┘ ┴ └──────────────────────────┘ ┴└───────┘ ┴└────────┘
src └─────┘ └──────────────────────────┘ └───────┘ └────────┘
typ └─────┘ ┴ └──────────────────────────┘ ┴└───────┘ ┴└────────┘
147
148 protected lemma subset_image {α β} (e : α ≃ β) (s : set α) (t : set β) : t ⊆ e '' s ↔ e.symm '' t ⊆ s :=
id ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴└───┘ └┘ ┴ ┴ ┴
src ┴ └─┘ └─┘ ┴ └┘ ┴ └───┘ └┘ ┴
typ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴└───┘ └┘ ┴ ┴ ┴
doc ┴
149 by rw [set.image_subset_iff, e.image_eq_preimage]
id └──────────────────┘
src └──┘└──────────────────┘└┘ └─
typ └──┘└──────────────────┘└┘└─────────────────┘└─
doc └──┘└──────────────────┘└┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └───────────────────────┘└───────────────────┘┴└
150
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
151 lemma symm_image_image {α β} (f : equiv α β) (s : set α) : f.symm '' (f '' s) = s :=
id └───┘ ┴ ┴ └─┘ ┴ ┴└───┘ └┘ ┴ └┘ ┴ ┴ ┴
src └───┘ └─┘ └───┘ └┘ └┘ ┴
typ └───┘ ┴ ┴ └─┘ ┴ ┴└───┘ └┘ ┴ └┘ ┴ ┴ ┴
doc └───┘
152 by { rw [← set.image_comp], simp }
id └────────────┘
src └────┘└────────────┘┴ └───┘
typ └────┘└────────────┘┴ └───┘
doc └────┘ ┴ └───┘
txt └────┘ ┴ └───┘
par └────┘ ┴ └───┘
pid └──┘ ┴ ┴
st └─────────────────────┘└──────┘└┘
153
154 protected lemma image_compl {α β} (f : equiv α β) (s : set α) :
id └───┘ ┴ ┴ └─┘ ┴
src └───┘ └─┘
typ └───┘ ┴ ┴ └─┘ ┴
doc └───┘
155 f '' -s = -(f '' s) :=
id ┴ └┘ ┴┴ ┴ ┴ ┴ └┘ ┴
src └┘ ┴ ┴ ┴ └┘
typ ┴ └┘ ┴┴ ┴ ┴ ┴ └┘ ┴
156 set.image_compl_eq f.bijective
id └────────────────┘ ┴└────────┘
src └────────────────┘ └────────┘
typ └────────────────┘ ┴└────────┘
157
158 /- The group of permutations (self-equivalences) of a type `α` -/
159
160 namespace perm
161
162 instance perm_group {α : Type u} : group (perm α) :=
id └───┘ └──┘ ┴
src └───┘ └──┘
typ └───┘ └──┘ ┴
doc └──┘
163 begin
st └─────
164 refine { mul := λ f g, equiv.trans g f, one := equiv.refl α, inv:= equiv.symm, ..};
id └─────────┘ └────────┘ ┴ └────────┘
src └─────┘ └──────┘ └────┘└─────────┘┴ ┴ └───────┘└────────┘┴ └──────┘└────────┘└───┘
typ └─────┘ └──────┘ └────┘└─────────┘┴ ┴ └───────┘└────────┘┴┴└──────┘└────────┘└───┘
doc └─────┘ └──────┘ └────┘ ┴ ┴ └───────┘ ┴ └──────┘ └───┘
txt └─────┘ └──────┘ └────┘ ┴ ┴ └───────┘ ┴ └──────┘ └───┘
par └─────┘ └──────┘ └────┘ ┴ ┴ └───────┘ ┴ └──────┘ └───┘
pid ┴ └──────┘ └────┘ ┴ ┴ └───────┘ ┴ └──────┘ └───┘
st ──────────────────────────────────────────────────────────────────────────────────────
165 intros; apply equiv.ext; try { apply trans_apply },
id └───────┘ └─────────┘
src └────┘ └────┘└───────┘ └────┘└────┘└─────────┘┴┴
typ └────┘ └────┘└───────┘ └────┘└────┘└─────────┘┴┴
doc └────┘ └────┘ └────┘└────┘ ┴┴
txt └────┘ └────┘ └────┘└────┘ ┴┴
par └────┘ └────┘ └────┘└────┘ ┴┴
pid ┴ └───────┘ └┘
st ───────────────────────────────┘└─────────────────┘└┘└
166 apply symm_apply_apply
id └──────────────┘
src └────┘└──────────────┘┴
typ └────┘└──────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ────────────────────────┘
167 end
st └─┘
168
169 @[simp] theorem mul_apply {α : Type u} (f g : perm α) (x) : (f * g) x = f (g x) :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └──┘
170 equiv.trans_apply _ _ _
id └───────────────┘
src └───────────────┘
typ └───────────────┘
171
172 @[simp] theorem one_apply {α : Type u} (x) : (1 : perm α) x = x := rfl
id └──┘ ┴ ┴ ┴ ┴ └─┘
src └──┘ ┴ └─┘
typ └──┘ ┴ ┴ ┴ ┴ └─┘
doc └──┘ └──┘
173
174 @[simp] lemma inv_apply_self {α : Type u} (f : perm α) (x) :
id └──┘ ┴
src └──┘
typ └──┘ ┴
doc └──┘ └──┘
175 f⁻¹ (f x) = x := equiv.symm_apply_apply _ _
id ┴└┘ ┴ ┴ ┴ ┴ └────────────────────┘
src └┘ ┴ └────────────────────┘
typ ┴└┘ ┴ ┴ ┴ ┴ └────────────────────┘
176
177 @[simp] lemma apply_inv_self {α : Type u} (f : perm α) (x) :
id └──┘ ┴
src └──┘
typ └──┘ ┴
doc └──┘ └──┘
178 f (f⁻¹ x) = x := equiv.apply_symm_apply _ _
id ┴ ┴└┘ ┴ ┴ ┴ └────────────────────┘
src └┘ ┴ └────────────────────┘
typ ┴ ┴└┘ ┴ ┴ ┴ └────────────────────┘
179
180 lemma one_def {α : Type u} : (1 : perm α) = equiv.refl α := rfl
id └──┘ ┴ ┴ └────────┘ ┴ └─┘
src └──┘ ┴ └────────┘ └─┘
typ └──┘ ┴ ┴ └────────┘ ┴ └─┘
doc └──┘
181
182 lemma mul_def {α : Type u} (f g : perm α) : f * g = g.trans f := rfl
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴└────┘ ┴ └─┘
src └──┘ ┴ ┴ └────┘ └─┘
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴└────┘ ┴ └─┘
doc └──┘
183
184 lemma inv_def {α : Type u} (f : perm α) : f⁻¹ = f.symm := rfl
id └──┘ ┴ ┴└┘ ┴ ┴└───┘ └─┘
src └──┘ └┘ ┴ └───┘ └─┘
typ └──┘ ┴ ┴└┘ ┴ ┴└───┘ └─┘
doc └──┘
185
186 end perm
187
188 def equiv_empty (h : α → false) : α ≃ empty :=
id ┴ └───┘ ┴ ┴ └───┘
src └───┘ ┴ └───┘
typ ┴ └───┘ ┴ ┴ └───┘
doc ┴
189 ⟨λ x, (h x).elim, λ e, e.rec _, λ x, (h x).elim, λ e, e.rec _⟩
id ┴ ┴ ┴ └──┘ ┴ ┴└──┘ ┴ ┴ ┴ └──┘ ┴ ┴└──┘
src └──┘ └──┘ └──┘ └──┘
typ ┴ ┴ ┴ └──┘ ┴ ┴└──┘ ┴ ┴ ┴ └──┘ ┴ ┴└──┘
190
191 def false_equiv_empty : false ≃ empty :=
id └───┘ ┴ └───┘
src └───┘ ┴ └───┘
typ └───┘ ┴ └───┘
doc ┴
192 equiv_empty _root_.id
id └─────────┘ └───────┘
src └─────────┘ └───────┘
typ └─────────┘ └───────┘
193
194 def equiv_pempty (h : α → false) : α ≃ pempty :=
id ┴ └───┘ ┴ ┴ └────┘
src └───┘ ┴ └────┘
typ ┴ └───┘ ┴ ┴ └────┘
doc ┴ └────┘
195 ⟨λ x, (h x).elim, λ e, e.rec _, λ x, (h x).elim, λ e, e.rec _⟩
id ┴ ┴ ┴ └──┘ ┴ ┴└──┘ ┴ ┴ ┴ └──┘ ┴ ┴└──┘
src └──┘ └──┘ └──┘ └──┘
typ ┴ ┴ ┴ └──┘ ┴ ┴└──┘ ┴ ┴ ┴ └──┘ ┴ ┴└──┘
196
197 def false_equiv_pempty : false ≃ pempty :=
id └───┘ ┴ └────┘
src └───┘ ┴ └────┘
typ └───┘ ┴ └────┘
doc ┴ └────┘
198 equiv_pempty _root_.id
id └──────────┘ └───────┘
src └──────────┘ └───────┘
typ └──────────┘ └───────┘
199
200 def empty_equiv_pempty : empty ≃ pempty :=
id └───┘ ┴ └────┘
src └───┘ ┴ └────┘
typ └───┘ ┴ └────┘
doc ┴ └────┘
201 equiv_pempty $ empty.rec _
id └──────────┘ └───────┘
src └──────────┘ └───────┘
typ └──────────┘ └───────┘
202
203 def pempty_equiv_pempty : pempty.{v} ≃ pempty.{w} :=
id └────┘ ┴ └────┘
src └────┘ ┴ └────┘
typ └────┘ ┴ └────┘
doc └────┘ ┴ └────┘
204 equiv_pempty pempty.elim
id └──────────┘ └─────────┘
src └──────────┘ └─────────┘
typ └──────────┘ └─────────┘
205
206 def empty_of_not_nonempty {α : Sort*} (h : ¬ nonempty α) : α ≃ empty :=
id ┴ └──────┘ ┴ ┴ ┴ └───┘
src ┴ └──────┘ ┴ └───┘
typ ┴ └──────┘ ┴ ┴ ┴ └───┘
doc ┴
207 equiv_empty $ assume a, h ⟨a⟩
id └─────────┘ ┴ ┴ ┴
src └─────────┘
typ └─────────┘ ┴ ┴ ┴
208
209 def pempty_of_not_nonempty {α : Sort*} (h : ¬ nonempty α) : α ≃ pempty :=
id ┴ └──────┘ ┴ ┴ ┴ └────┘
src ┴ └──────┘ ┴ └────┘
typ ┴ └──────┘ ┴ ┴ ┴ └────┘
doc ┴ └────┘
210 equiv_pempty $ assume a, h ⟨a⟩
id └──────────┘ ┴ ┴ ┴
src └──────────┘
typ └──────────┘ ┴ ┴ ┴
211
212 def prop_equiv_punit {p : Prop} (h : p) : p ≃ punit :=
id ┴ ┴ ┴ └───┘
src ┴ └───┘
typ ┴ ┴ ┴ └───┘
doc ┴
213 ⟨λ x, (), λ x, h, λ _, rfl, λ ⟨⟩, rfl⟩
id ┴ └┘ ┴ ┴ ┴ └─┘ ┴ └─┘
src └┘ └─┘ ┴ └─┘
typ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ └─┘
214
215 def true_equiv_punit : true ≃ punit := prop_equiv_punit trivial
id └──┘ ┴ └───┘ └──────────────┘ └─────┘
src └──┘ ┴ └───┘ └──────────────┘ └─────┘
typ └──┘ ┴ └───┘ └──────────────┘ └─────┘
doc ┴
216
217 protected def ulift {α : Type u} : ulift α ≃ α :=
id └───┘ ┴ ┴ ┴
src └───┘ ┴
typ └───┘ ┴ ┴ ┴
doc └───┘ ┴
218 ⟨ulift.down, ulift.up, ulift.up_down, λ a, rfl⟩
id └────────┘ └──────┘ └───────────┘ ┴ └─┘
src └────────┘ └──────┘ └───────────┘ └─┘
typ └────────┘ └──────┘ └───────────┘ ┴ └─┘
219
220 protected def plift : plift α ≃ α :=
id └───┘ ┴ ┴ ┴
src └───┘ ┴
typ └───┘ ┴ ┴ ┴
doc └───┘ ┴
221 ⟨plift.down, plift.up, plift.up_down, plift.down_up⟩
id └────────┘ └──────┘ └───────────┘ └───────────┘
src └────────┘ └──────┘ └───────────┘ └───────────┘
typ └────────┘ └──────┘ └───────────┘ └───────────┘
222
223 @[congr] def arrow_congr {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) :
id └┘ ┴ └┘ └┘ ┴ └┘
src └───┘ ┴ ┴
typ └┘ ┴ └┘ └┘ ┴ └┘
doc └───┘ ┴ ┴
224 (α₁ → β₁) ≃ (α₂ → β₂) :=
id └┘ └┘ ┴ └┘ └┘
src ┴
typ └┘ └┘ ┴ └┘ └┘
doc ┴
225 { to_fun := λ f, e₂.to_fun ∘ f ∘ e₁.inv_fun,
id ┴ └┘└─────┘ ┴ ┴ ┴ └┘└──────┘
src └─────┘ ┴ ┴ └──────┘
typ ┴ └┘└─────┘ ┴ ┴ ┴ └┘└──────┘
226 inv_fun := λ f, e₂.inv_fun ∘ f ∘ e₁.to_fun,
id ┴ └┘└──────┘ ┴ ┴ ┴ └┘└─────┘
src └──────┘ ┴ ┴ └─────┘
typ ┴ └┘└──────┘ ┴ ┴ ┴ └┘└─────┘
227 left_inv := λ f, funext $ λ x, by { dsimp, rw [e₂.left_inv, e₁.left_inv] },
id ┴ └────┘ ┴
src └────┘ └───┘ └──┘ └┘ └┘
typ ┴ └────┘ ┴ └───┘ └──┘└─────────┘└┘└─────────┘└┘
doc └───┘ └──┘ └┘ └┘
txt └───┘ └──┘ └┘ └┘
par └───┘ └──┘ └┘ └┘
pid └┘ └┘ ┴┴
st └──────┘└───────────────┘└───────────┘┴┴└┘
228 right_inv := λ f, funext $ λ x, by { dsimp, rw [e₂.right_inv, e₁.right_inv] } }
id ┴ └────┘ ┴
src └────┘ └───┘ └──┘ └┘ └┘
typ ┴ └────┘ ┴ └───┘ └──┘└──────────┘└┘└──────────┘└┘
doc └───┘ └──┘ └┘ └┘
txt └───┘ └──┘ └┘ └┘
par └───┘ └──┘ └┘ └┘
pid └┘ └┘ ┴┴
st └──────┘└────────────────┘└────────────┘┴┴└┘
229
230 @[simp] lemma arrow_congr_apply {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂)
id └┘ ┴ └┘ └┘ ┴ └┘
src ┴ ┴
typ └┘ ┴ └┘ └┘ ┴ └┘
doc └──┘ ┴ ┴
231 (f : α₁ → β₁) (x : α₂) :
id └┘ └┘ └┘
typ └┘ └┘ └┘
232 arrow_congr e₁ e₂ f x = (e₂ $ f $ e₁.symm x) :=
id └─────────┘ └┘ └┘ ┴ ┴ ┴ └┘ ┴ └┘└───┘ ┴
src └─────────┘ ┴ └───┘
typ └─────────┘ └┘ └┘ ┴ ┴ ┴ └┘ ┴ └┘└───┘ ┴
233 rfl
id └─┘
src └─┘
typ └─┘
234
235 lemma arrow_congr_comp {α₁ β₁ γ₁ α₂ β₂ γ₂ : Sort*}
236 (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) (ec : γ₁ ≃ γ₂) (f : α₁ → β₁) (g : β₁ → γ₁) :
id └┘ ┴ └┘ └┘ ┴ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘
src ┴ ┴ ┴
typ └┘ ┴ └┘ └┘ ┴ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘
doc ┴ ┴ ┴
237 arrow_congr ea ec (g ∘ f) = (arrow_congr eb ec g) ∘ (arrow_congr ea eb f) :=
id └─────────┘ └┘ └┘ ┴ ┴ ┴ ┴ └─────────┘ └┘ └┘ ┴ ┴ └─────────┘ └┘ └┘ ┴
src └─────────┘ ┴ ┴ └─────────┘ ┴ └─────────┘
typ └─────────┘ └┘ └┘ ┴ ┴ ┴ ┴ └─────────┘ └┘ └┘ ┴ ┴ └─────────┘ └┘ └┘ ┴
238 by { ext, simp only [comp, arrow_congr_apply, eb.symm_apply_apply] }
id └──┘ └───────────────┘
src └─┘ └─────────┘└──┘└┘└───────────────┘└┘ └┘
typ └─┘ └─────────┘└──┘└┘└───────────────┘└┘└─────────────────┘└┘
doc └─┘ └─────────┘ └┘ └┘ └┘
txt └─┘ └─────────┘ └┘ └┘ └┘
par └─┘ └─────────┘ └┘ └┘ └┘
pid ┴└──┘└┘ └┘ └┘ ┴┴
st └────┘└─────────────────────────────────────────────────────────┘└┘
239
240 @[simp] lemma arrow_congr_refl {α β : Sort*} :
doc └──┘
241 arrow_congr (equiv.refl α) (equiv.refl β) = equiv.refl (α → β) := rfl
id └─────────┘ └────────┘ ┴ └────────┘ ┴ ┴ └────────┘ ┴ ┴ └─┘
src └─────────┘ └────────┘ └────────┘ ┴ └────────┘ └─┘
typ └─────────┘ └────────┘ ┴ └────────┘ ┴ ┴ └────────┘ ┴ ┴ └─┘
242
243 @[simp] lemma arrow_congr_trans {α₁ β₁ α₂ β₂ α₃ β₃ : Sort*}
doc └──┘
244 (e₁ : α₁ ≃ α₂) (e₁' : β₁ ≃ β₂) (e₂ : α₂ ≃ α₃) (e₂' : β₂ ≃ β₃) :
id └┘ ┴ └┘ └┘ ┴ └┘ └┘ ┴ └┘ └┘ ┴ └┘
src ┴ ┴ ┴ ┴
typ └┘ ┴ └┘ └┘ ┴ └┘ └┘ ┴ └┘ └┘ ┴ └┘
doc ┴ ┴ ┴ ┴
245 arrow_congr (e₁.trans e₂) (e₁'.trans e₂') = (arrow_congr e₁ e₁').trans (arrow_congr e₂ e₂') :=
id └─────────┘ └┘└────┘ └┘ └─┘└────┘ └─┘ ┴ └─────────┘ └┘ └─┘ └───┘ └─────────┘ └┘ └─┘
src └─────────┘ └────┘ └────┘ ┴ └─────────┘ └───┘ └─────────┘
typ └─────────┘ └┘└────┘ └┘ └─┘└────┘ └─┘ ┴ └─────────┘ └┘ └─┘ └───┘ └─────────┘ └┘ └─┘
246 rfl
id └─┘
src └─┘
typ └─┘
247
248 @[simp] lemma arrow_congr_symm {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) :
id └┘ ┴ └┘ └┘ ┴ └┘
src ┴ ┴
typ └┘ ┴ └┘ └┘ ┴ └┘
doc └──┘ ┴ ┴
249 (arrow_congr e₁ e₂).symm = arrow_congr e₁.symm e₂.symm :=
id └─────────┘ └┘ └┘ └──┘ ┴ └─────────┘ └┘└───┘ └┘└───┘
src └─────────┘ └──┘ ┴ └─────────┘ └───┘ └───┘
typ └─────────┘ └┘ └┘ └──┘ ┴ └─────────┘ └┘└───┘ └┘└───┘
250 rfl
id └─┘
src └─┘
typ └─┘
251
252 def conj (e : α ≃ β) : (α → α) ≃ (β → β) := arrow_congr e e
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘ ┴ ┴
src ┴ ┴ └─────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘ ┴ ┴
doc ┴ ┴
253
254 @[simp] lemma conj_apply (e : α ≃ β) (f : α → α) (x : β) :
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ ┴
255 e.conj f x = (e $ f $ e.symm x) :=
id ┴└───┘ ┴ ┴ ┴ ┴ ┴ ┴└───┘ ┴
src └───┘ ┴ └───┘
typ ┴└───┘ ┴ ┴ ┴ ┴ ┴ ┴└───┘ ┴
256 rfl
id └─┘
src └─┘
typ └─┘
257
258 @[simp] lemma conj_refl : conj (equiv.refl α) = equiv.refl (α → α) := rfl
id └──┘ └────────┘ ┴ ┴ └────────┘ ┴ ┴ └─┘
src └──┘ └────────┘ ┴ └────────┘ └─┘
typ └──┘ └────────┘ ┴ ┴ └────────┘ ┴ ┴ └─┘
doc └──┘
259
260 @[simp] lemma conj_symm (e : α ≃ β) : e.conj.symm = e.symm.conj := rfl
id ┴ ┴ ┴ ┴└───┘└───┘ ┴ ┴└───┘└───┘ └─┘
src ┴ └───┘└───┘ ┴ └───┘└───┘ └─┘
typ ┴ ┴ ┴ ┴└───┘└───┘ ┴ ┴└───┘└───┘ └─┘
doc └──┘ ┴
261
262 @[simp] lemma conj_trans (e₁ : α ≃ β) (e₂ : β ≃ γ) :
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ ┴ ┴
263 (e₁.trans e₂).conj = e₁.conj.trans e₂.conj :=
id └┘└────┘ └┘ └──┘ ┴ └┘└───┘└────┘ └┘└───┘
src └────┘ └──┘ ┴ └───┘└────┘ └───┘
typ └┘└────┘ └┘ └──┘ ┴ └┘└───┘└────┘ └┘└───┘
264 rfl
id └─┘
src └─┘
typ └─┘
265
266 @[simp] lemma conj_comp (e : α ≃ β) (f₁ f₂ : α → α) :
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
doc └──┘ ┴
267 e.conj (f₁ ∘ f₂) = (e.conj f₁) ∘ (e.conj f₂) :=
id ┴└───┘ └┘ ┴ └┘ ┴ ┴└───┘ └┘ ┴ ┴└───┘ └┘
src └───┘ ┴ ┴ └───┘ ┴ └───┘
typ ┴└───┘ └┘ ┴ └┘ ┴ ┴└───┘ └┘ ┴ ┴└───┘ └┘
268 by apply arrow_congr_comp
id └──────────────┘
src └────┘└──────────────┘└
typ └────┘└──────────────┘└
doc └────┘ └
txt └────┘ └
par └────┘ └
pid ┴ └
st └───────────────────────
269
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
270 def punit_equiv_punit : punit.{v} ≃ punit.{w} :=
id └───┘ ┴ └───┘
src └───┘ ┴ └───┘
typ └───┘ ┴ └───┘
doc ┴
271 ⟨λ _, punit.star, λ _, punit.star, λ u, by { cases u, refl }, λ u, by { cases u, reflexivity }⟩
id ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴
src └────────┘ └────────┘ └────┘ └───┘ └────┘ └──────────┘
typ ┴ └────────┘ ┴ └────────┘ ┴ └────┘┴ └───┘ ┴ └────┘┴ └──────────┘
doc └────┘ └───┘ └────┘ └──────────┘
txt └────┘ └───┘ └────┘ └──────────┘
par └────┘ └───┘ └────┘ └──────────┘
pid ┴ ┴ ┴ ┴
st └────────┘└─────┘└┘ └────────┘└────────────┘└┘
272
273 section
274 @[simp] def arrow_punit_equiv_punit (α : Sort*) : (α → punit.{v}) ≃ punit.{w} :=
id ┴ └───┘ ┴ └───┘
src └───┘ ┴ └───┘
typ ┴ └───┘ ┴ └───┘
doc └──┘ ┴
275 ⟨λ f, punit.star, λ u f, punit.star,
id ┴ └────────┘ ┴ ┴ └────────┘
src └────────┘ └────────┘
typ ┴ └────────┘ ┴ ┴ └────────┘
276 λ f, by { funext x, cases f x, refl }, λ u, by { cases u, reflexivity }⟩
id ┴ ┴ ┴ ┴ ┴
src └──────┘ └────┘ ┴ └───┘ └────┘ └──────────┘
typ ┴ └──────┘ └────┘┴┴┴ └───┘ ┴ └────┘┴ └──────────┘
doc └──────┘ └────┘ ┴ └───┘ └────┘ └──────────┘
txt └──────┘ └────┘ ┴ └───┘ └────┘ └──────────┘
par └──────┘ └────┘ ┴ └───┘ └────┘ └──────────┘
pid └┘ ┴ ┴ ┴ ┴ ┴
st └─────────┘└─────────┘└─────┘└┘ └────────┘└────────────┘└┘
277
278 @[simp] def punit_arrow_equiv (α : Sort*) : (punit.{u} → α) ≃ α :=
id └───┘ ┴ ┴ ┴
src └───┘ ┴
typ └───┘ ┴ ┴ ┴
doc └──┘ ┴
279 ⟨λ f, f punit.star, λ a u, a, λ f, by { funext x, cases x, refl }, λ u, rfl⟩
id ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
src └────────┘ └──────┘ └────┘ └───┘ └─┘
typ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ └──────┘ └────┘┴ └───┘ ┴ └─┘
doc └──────┘ └────┘ └───┘
txt └──────┘ └────┘ └───┘
par └──────┘ └────┘ └───┘
pid └┘ ┴ ┴
st └─────────┘└───────┘└─────┘└┘
280
281 @[simp] def empty_arrow_equiv_punit (α : Sort*) : (empty → α) ≃ punit.{u} :=
id └───┘ ┴ ┴ └───┘
src └───┘ ┴ └───┘
typ └───┘ ┴ ┴ └───┘
doc └──┘ ┴
282 ⟨λ f, punit.star, λ u e, e.rec _, λ f, funext $ λ x, x.rec _, λ u, by { cases u, refl }⟩
id ┴ └────────┘ ┴ ┴ ┴└──┘ ┴ └────┘ ┴ ┴└──┘ ┴ ┴
src └────────┘ └──┘ └────┘ └──┘ └────┘ └───┘
typ ┴ └────────┘ ┴ ┴ ┴└──┘ ┴ └────┘ ┴ ┴└──┘ ┴ └────┘┴ └───┘
doc └────┘ └───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴ ┴
st └────────┘└─────┘└┘
283
284 @[simp] def pempty_arrow_equiv_punit (α : Sort*) : (pempty → α) ≃ punit.{u} :=
id └────┘ ┴ ┴ └───┘
src └────┘ ┴ └───┘
typ └────┘ ┴ ┴ └───┘
doc └──┘ └────┘ ┴
285 ⟨λ f, punit.star, λ u e, e.rec _, λ f, funext $ λ x, x.rec _, λ u, by { cases u, refl }⟩
id ┴ └────────┘ ┴ ┴ ┴└──┘ ┴ └────┘ ┴ ┴└──┘ ┴ ┴
src └────────┘ └──┘ └────┘ └──┘ └────┘ └───┘
typ ┴ └────────┘ ┴ ┴ ┴└──┘ ┴ └────┘ ┴ ┴└──┘ ┴ └────┘┴ └───┘
doc └────┘ └───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴ ┴
st └────────┘└─────┘└┘
286
287 @[simp] def false_arrow_equiv_punit (α : Sort*) : (false → α) ≃ punit.{u} :=
id └───┘ ┴ ┴ └───┘
src └───┘ ┴ └───┘
typ └───┘ ┴ ┴ └───┘
doc └──┘ ┴
288 calc (false → α) ≃ (empty → α) : arrow_congr false_equiv_empty (equiv.refl _)
id └───┘ ┴ └───┘ ┴ └─────────┘ └───────────────┘ └────────┘
src └───┘ └───┘ └─────────┘ └───────────────┘ └────────┘
typ └───┘ ┴ └───┘ ┴ └─────────┘ └───────────────┘ └────────┘
289 ... ≃ punit : empty_arrow_equiv_punit _
id └───┘ └─────────────────────┘
src └───┘ └─────────────────────┘
typ └───┘ └─────────────────────┘
290
291 end
292
293 @[congr] def prod_congr {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ :β₁ ≃ β₂) : α₁ × β₁ ≃ α₂ × β₂ :=
id └┘ ┴ └┘ └┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴ └┘
src └───┘ ┴ ┴ ┴ ┴ ┴
typ └┘ ┴ └┘ └┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴ └┘
doc └───┘ ┴ ┴ ┴
294 ⟨λp, (e₁ p.1, e₂ p.2), λp, (e₁.symm p.1, e₂.symm p.2),
id ┴ ┴└┘ ┴┴ └┘ ┴┴ ┴ ┴└┘└───┘ ┴┴ └┘└───┘ ┴┴
src ┴ ┴ ┴ ┴ └───┘ ┴ └───┘ ┴
typ ┴ ┴└┘ ┴┴ └┘ ┴┴ ┴ ┴└┘└───┘ ┴┴ └┘└───┘ ┴┴
295 λ ⟨a, b⟩, show (e₁.symm (e₁ a), e₂.symm (e₂ b)) = (a, b), by rw [symm_apply_apply, symm_apply_apply],
id ┴┴ ┴ ┴└┘└───┘ └┘ └┘└───┘ └┘ ┴ ┴ └──────────────┘ └──────────────┘
src ┴ └───┘ └───┘ ┴ ┴ └──┘└──────────────┘└┘└──────────────┘┴
typ ┴┴ ┴ ┴└┘└───┘ └┘ └┘└───┘ └┘ ┴ ┴ └──┘└──────────────┘└┘└──────────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st └───────────────────┘└────────────────┘┴
296 λ ⟨a, b⟩, show (e₁ (e₁.symm a), e₂ (e₂.symm b)) = (a, b), by rw [apply_symm_apply, apply_symm_apply]⟩
id ┴┴ ┴ ┴└┘ └┘└───┘ └┘ └┘└───┘ ┴ ┴ └──────────────┘ └──────────────┘
src ┴ └───┘ └───┘ ┴ ┴ └──┘└──────────────┘└┘└──────────────┘┴
typ ┴┴ ┴ ┴└┘ └┘└───┘ └┘ └┘└───┘ ┴ ┴ └──┘└──────────────┘└┘└──────────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st └───────────────────┘└────────────────┘┴
297
298 @[simp] theorem prod_congr_apply {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) (a : α₁) (b : β₁) :
id └┘ ┴ └┘ └┘ ┴ └┘ └┘ └┘
src ┴ ┴
typ └┘ ┴ └┘ └┘ ┴ └┘ └┘ └┘
doc └──┘ ┴ ┴
299 prod_congr e₁ e₂ (a, b) = (e₁ a, e₂ b) :=
id └────────┘ └┘ └┘ ┴┴ ┴ ┴ ┴└┘ ┴ └┘ ┴
src └────────┘ ┴ ┴ ┴
typ └────────┘ └┘ └┘ ┴┴ ┴ ┴ ┴└┘ ┴ └┘ ┴
300 rfl
id └─┘
src └─┘
typ └─┘
301
302 @[simp] def prod_comm (α β : Sort*) : α × β ≃ β × α :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ ┴
303 ⟨λ p, (p.2, p.1), λ p, (p.2, p.1), λ⟨a, b⟩, rfl, λ⟨a, b⟩, rfl⟩
id ┴ ┴┴┴ ┴┴ ┴ ┴┴┴ ┴┴ ┴ └─┘ ┴ └─┘
src ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └─┘
typ ┴ ┴┴┴ ┴┴ ┴ ┴┴┴ ┴┴ ┴ └─┘ ┴ └─┘
304
305 @[simp] def prod_assoc (α β γ : Sort*) : (α × β) × γ ≃ α × (β × γ) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ ┴
306 ⟨λ p, ⟨p.1.1, ⟨p.1.2, p.2⟩⟩, λp, ⟨⟨p.1, p.2.1⟩, p.2.2⟩, λ ⟨⟨a, b⟩, c⟩, rfl, λ ⟨a, ⟨b, c⟩⟩, rfl⟩
id ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴┴ ┴ ┴┴ ┴ ┴ └─┘ ┴ └─┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └─┘
typ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴┴ ┴ ┴┴ ┴ ┴ └─┘ ┴ └─┘
307
308 @[simp] theorem prod_assoc_apply {α β γ : Sort*} (p : (α × β) × γ) :
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
doc └──┘
309 prod_assoc α β γ p = ⟨p.1.1, ⟨p.1.2, p.2⟩⟩ := rfl
id └────────┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ └─┘
src └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
typ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ └─┘
310
311 section
312 @[simp] def prod_punit (α : Sort*) : α × punit.{u+1} ≃ α :=
id ┴ ┴ └───┘ ┴ ┴
src ┴ └───┘ ┴
typ ┴ ┴ └───┘ ┴ ┴
doc └──┘ ┴
313 ⟨λ p, p.1, λ a, (a, punit.star), λ ⟨_, punit.star⟩, rfl, λ a, rfl⟩
id ┴ ┴┴ ┴ ┴┴ └────────┘ ┴ └────────┘ └─┘ ┴ └─┘
src ┴ ┴ └────────┘ └────────┘ └─┘ └─┘
typ ┴ ┴┴ ┴ ┴┴ └────────┘ ┴ └────────┘ └─┘ ┴ └─┘
314
315 @[simp] theorem prod_punit_apply {α : Sort*} (a : α × punit.{u+1}) : prod_punit α a = a.1 := rfl
id ┴ ┴ └───┘ └────────┘ ┴ ┴ ┴ ┴┴ └─┘
src ┴ └───┘ └────────┘ ┴ ┴ └─┘
typ ┴ ┴ └───┘ └────────┘ ┴ ┴ ┴ ┴┴ └─┘
doc └──┘
316
317 @[simp] def punit_prod (α : Sort*) : punit.{u+1} × α ≃ α :=
id └───┘ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴
doc └──┘ ┴
318 calc punit × α ≃ α × punit : prod_comm _ _
id └───┘ ┴ ┴ ┴ ┴ └───┘ └───────┘
src └───┘ ┴ ┴ └───┘ └───────┘
typ └───┘ ┴ ┴ ┴ ┴ └───┘ └───────┘
319 ... ≃ α : prod_punit _
id ┴ └────────┘
src └────────┘
typ ┴ └────────┘
320
321 @[simp] theorem punit_prod_apply {α : Sort*} (a : punit.{u+1} × α) : punit_prod α a = a.2 := rfl
id └───┘ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴┴ └─┘
src └───┘ ┴ └────────┘ ┴ ┴ └─┘
typ └───┘ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴┴ └─┘
doc └──┘
322
323 @[simp] def prod_empty (α : Sort*) : α × empty ≃ empty :=
id ┴ ┴ └───┘ ┴ └───┘
src ┴ └───┘ ┴ └───┘
typ ┴ ┴ └───┘ ┴ └───┘
doc └──┘ ┴
324 equiv_empty (λ ⟨_, e⟩, e.rec _)
id └─────────┘ ┴ ┴ └──┘
src └─────────┘ └──┘
typ └─────────┘ ┴ ┴ └──┘
325
326 @[simp] def empty_prod (α : Sort*) : empty × α ≃ empty :=
id └───┘ ┴ ┴ ┴ └───┘
src └───┘ ┴ ┴ └───┘
typ └───┘ ┴ ┴ ┴ └───┘
doc └──┘ ┴
327 equiv_empty (λ ⟨e, _⟩, e.rec _)
id └─────────┘ ┴┴ └──┘
src └─────────┘ └──┘
typ └─────────┘ ┴┴ └──┘
328
329 @[simp] def prod_pempty (α : Sort*) : α × pempty ≃ pempty :=
id ┴ ┴ └────┘ ┴ └────┘
src ┴ └────┘ ┴ └────┘
typ ┴ ┴ └────┘ ┴ └────┘
doc └──┘ └────┘ ┴ └────┘
330 equiv_pempty (λ ⟨_, e⟩, e.rec _)
id └──────────┘ ┴ ┴ └──┘
src └──────────┘ └──┘
typ └──────────┘ ┴ ┴ └──┘
331
332 @[simp] def pempty_prod (α : Sort*) : pempty × α ≃ pempty :=
id └────┘ ┴ ┴ ┴ └────┘
src └────┘ ┴ ┴ └────┘
typ └────┘ ┴ ┴ ┴ └────┘
doc └──┘ └────┘ ┴ └────┘
333 equiv_pempty (λ ⟨e, _⟩, e.rec _)
id └──────────┘ ┴┴ └──┘
src └──────────┘ └──┘
typ └──────────┘ ┴┴ └──┘
334 end
335
336 section
337 open sum
338 def psum_equiv_sum (α β : Sort*) : psum α β ≃ α ⊕ β :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
339 ⟨λ s, psum.cases_on s inl inr,
id ┴ └───────────┘ ┴ └─┘ └─┘
src └───────────┘ └─┘ └─┘
typ ┴ └───────────┘ ┴ └─┘ └─┘
340 λ s, sum.cases_on s psum.inl psum.inr,
id ┴ └──────────┘ ┴ └──────┘ └──────┘
src └──────────┘ └──────┘ └──────┘
typ ┴ └──────────┘ ┴ └──────┘ └──────┘
341 λ s, by cases s; refl,
id ┴ ┴
src └────┘ └──┘
typ ┴ └────┘┴ └──┘
doc └────┘ └──┘
txt └────┘ └──┘
par └────┘ └──┘
pid ┴
st └────────────┘
342 λ s, by cases s; refl⟩
id ┴ ┴
src └────┘ └──┘
typ ┴ └────┘┴ └──┘
doc └────┘ └──┘
txt └────┘ └──┘
par └────┘ └──┘
pid ┴
st └────────────┘
343
344 def sum_congr {α₁ β₁ α₂ β₂ : Sort*} : α₁ ≃ α₂ → β₁ ≃ β₂ → α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
id └┘ ┴ └┘ ┴ └┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴ └┘
src ┴ ┴ ┴ ┴ ┴
typ └┘ ┴ └┘ ┴ └┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴ └┘
doc ┴ ┴ ┴
345 | ⟨f₁, g₁, l₁, r₁⟩ ⟨f₂, g₂, l₂, r₂⟩ :=
id └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘
typ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘
346 ⟨λ s, match s with inl a₁ := inl (f₁ a₁) | inr b₁ := inr (f₂ b₁) end,
id ┴ ┴ └─┘ └┘ └─┘ └─┘ └┘ └─┘
src └─┘ └─┘ └─┘ └─┘
typ ┴ ┴ └─┘ └┘ └─┘ └─┘ └┘ └─┘
347 λ s, match s with inl a₂ := inl (g₁ a₂) | inr b₂ := inr (g₂ b₂) end,
id ┴ ┴ └─┘ └┘ └─┘ └─┘ └┘ └─┘
src └─┘ └─┘ └─┘ └─┘
typ ┴ ┴ └─┘ └┘ └─┘ └─┘ └┘ └─┘
348 λ s, match s with inl a := congr_arg inl (l₁ a) | inr a := congr_arg inr (l₂ a) end,
id ┴ ┴ └─┘ ┴ └───────┘ └─┘ └─┘ ┴ └───────┘ └─┘
src └─┘ └───────┘ └─┘ └─┘ └───────┘ └─┘
typ ┴ ┴ └─┘ ┴ └───────┘ └─┘ └─┘ ┴ └───────┘ └─┘
349 λ s, match s with inl a := congr_arg inl (r₁ a) | inr a := congr_arg inr (r₂ a) end⟩
id ┴ ┴ └─┘ ┴ └───────┘ └─┘ └─┘ ┴ └───────┘ └─┘
src └─┘ └───────┘ └─┘ └─┘ └───────┘ └─┘
typ ┴ ┴ └─┘ ┴ └───────┘ └─┘ └─┘ ┴ └───────┘ └─┘
350
351 @[simp] theorem sum_congr_apply_inl {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) (a : α₁) :
id └┘ ┴ └┘ └┘ ┴ └┘ └┘
src ┴ ┴
typ └┘ ┴ └┘ └┘ ┴ └┘ └┘
doc └──┘ ┴ ┴
352 sum_congr e₁ e₂ (inl a) = inl (e₁ a) :=
id └───────┘ └┘ └┘ └─┘ ┴ ┴ └─┘ └┘ ┴
src └───────┘ └─┘ ┴ └─┘
typ └───────┘ └┘ └┘ └─┘ ┴ ┴ └─┘ └┘ ┴
353 by { cases e₁, cases e₂, refl }
id └┘ └┘
src └────┘ └────┘ └───┘
typ └────┘└┘ └────┘└┘ └───┘
doc └────┘ └────┘ └───┘
txt └────┘ └────┘ └───┘
par └────┘ └────┘ └───┘
pid ┴ ┴ ┴
st └─────────┘└────────┘└─────┘└┘
354
355 @[simp] theorem sum_congr_apply_inr {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) (b : β₁) :
id └┘ ┴ └┘ └┘ ┴ └┘ └┘
src ┴ ┴
typ └┘ ┴ └┘ └┘ ┴ └┘ └┘
doc └──┘ ┴ ┴
356 sum_congr e₁ e₂ (inr b) = inr (e₂ b) :=
id └───────┘ └┘ └┘ └─┘ ┴ ┴ └─┘ └┘ ┴
src └───────┘ └─┘ ┴ └─┘
typ └───────┘ └┘ └┘ └─┘ ┴ ┴ └─┘ └┘ ┴
357 by { cases e₁, cases e₂, refl }
id └┘ └┘
src └────┘ └────┘ └───┘
typ └────┘└┘ └────┘└┘ └───┘
doc └────┘ └────┘ └───┘
txt └────┘ └────┘ └───┘
par └────┘ └────┘ └───┘
pid ┴ ┴ ┴
st └─────────┘└────────┘└─────┘└┘
358
359 @[simp] lemma sum_congr_symm {α β γ δ : Type u} (e : α ≃ β) (f : γ ≃ δ) (x) :
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ ┴ ┴
360 (equiv.sum_congr e f).symm x = (equiv.sum_congr (e.symm) (f.symm)) x :=
id └─────────────┘ ┴ ┴ └──┘ ┴ ┴ └─────────────┘ ┴└───┘ ┴└───┘ ┴
src └─────────────┘ └──┘ ┴ └─────────────┘ └───┘ └───┘
typ └─────────────┘ ┴ ┴ └──┘ ┴ ┴ └─────────────┘ ┴└───┘ ┴└───┘ ┴
361 by { cases e, cases f, cases x; refl }
id ┴ ┴ ┴
src └────┘ └────┘ └────┘ └───┘
typ └────┘┴ └────┘┴ └────┘┴ └───┘
doc └────┘ └────┘ └────┘ └───┘
txt └────┘ └────┘ └────┘ └───┘
par └────┘ └────┘ └────┘ └───┘
pid ┴ ┴ ┴ ┴
st └────────┘└───────┘└──────────────┘└┘
362
363 def bool_equiv_punit_sum_punit : bool ≃ punit.{u+1} ⊕ punit.{v+1} :=
id └──┘ ┴ └───┘ ┴ └───┘
src └──┘ ┴ └───┘ ┴ └───┘
typ └──┘ ┴ └───┘ ┴ └───┘
doc ┴
364 ⟨λ b, cond b (inr punit.star) (inl punit.star),
id ┴ └──┘ ┴ └─┘ └────────┘ └─┘ └────────┘
src └──┘ └─┘ └────────┘ └─┘ └────────┘
typ ┴ └──┘ ┴ └─┘ └────────┘ └─┘ └────────┘
365 λ s, sum.rec_on s (λ_, ff) (λ_, tt),
id ┴ └────────┘ ┴ ┴ └┘ ┴ └┘
src └────────┘ └┘ └┘
typ ┴ └────────┘ ┴ ┴ └┘ ┴ └┘
366 λ b, by cases b; refl,
id ┴ ┴
src └────┘ └──┘
typ ┴ └────┘┴ └──┘
doc └────┘ └──┘
txt └────┘ └──┘
par └────┘ └──┘
pid ┴
st └────────────┘
367 λ s, by rcases s with ⟨⟨⟩⟩ | ⟨⟨⟩⟩; refl⟩
id ┴ ┴
src └─────┘ └───────────────┘ └──┘
typ ┴ └─────┘┴└───────────────┘ └──┘
doc └─────┘ └───────────────┘ └──┘
txt └─────┘ └───────────────┘ └──┘
par └─────┘ └───────────────┘ └──┘
pid ┴ └───────────────┘
st └──────────────────────────────┘
368
369 noncomputable def Prop_equiv_bool : Prop ≃ bool :=
id ┴ └──┘
src ┴ └──┘
typ ┴ └──┘
doc ┴
370 ⟨λ p, @to_bool p (classical.prop_decidable _),
id ┴ └─────┘ ┴ └──────────────────────┘
src └─────┘ └──────────────────────┘
typ ┴ └─────┘ ┴ └──────────────────────┘
371 λ b, b, λ p, by simp, λ b, by simp⟩
id ┴ ┴ ┴ ┴
src └──┘ └──┘
typ ┴ ┴ ┴ └──┘ ┴ └──┘
doc └──┘ └──┘
txt └──┘ └──┘
par └──┘ └──┘
st └───┘ └───┘
372
373 @[simp] def sum_comm (α β : Sort*) : α ⊕ β ≃ β ⊕ α :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ ┴
374 ⟨λ s, match s with inl a := inr a | inr b := inl b end,
id ┴ ┴ └─┘ ┴ └─┘ └─┘ ┴ └─┘
src └─┘ └─┘ └─┘ └─┘
typ ┴ ┴ └─┘ ┴ └─┘ └─┘ ┴ └─┘
375 λ s, match s with inl b := inr b | inr a := inl a end,
id ┴ ┴ └─┘ ┴ └─┘ └─┘ ┴ └─┘
src └─┘ └─┘ └─┘ └─┘
typ ┴ ┴ └─┘ ┴ └─┘ └─┘ ┴ └─┘
376 λ s, by cases s; refl,
id ┴ ┴
src └────┘ └──┘
typ ┴ └────┘┴ └──┘
doc └────┘ └──┘
txt └────┘ └──┘
par └────┘ └──┘
pid ┴
st └────────────┘
377 λ s, by cases s; refl⟩
id ┴ ┴
src └────┘ └──┘
typ ┴ └────┘┴ └──┘
doc └────┘ └──┘
txt └────┘ └──┘
par └────┘ └──┘
pid ┴
st └────────────┘
378
379 @[simp] def sum_assoc (α β γ : Sort*) : (α ⊕ β) ⊕ γ ≃ α ⊕ (β ⊕ γ) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ ┴
380 ⟨λ s, match s with inl (inl a) := inl a | inl (inr b) := inr (inl b) | inr c := inr (inr c) end,
id ┴ ┴ └─┘ ┴ └─┘ └─┘ └─┘ ┴ └─┘ └─┘ └─┘ ┴ └─┘ └─┘
src └─┘ └─┘ └─┘ └─┘ └─┘ └─┘ └─┘ └─┘ └─┘
typ ┴ ┴ └─┘ ┴ └─┘ └─┘ └─┘ ┴ └─┘ └─┘ └─┘ ┴ └─┘ └─┘
381 λ s, match s with inl a := inl (inl a) | inr (inl b) := inl (inr b) | inr (inr c) := inr c end,
id ┴ ┴ └─┘ ┴ └─┘ └─┘ └─┘ └─┘ ┴ └─┘ └─┘ └─┘ ┴ └─┘
src └─┘ └─┘ └─┘ └─┘ └─┘ └─┘ └─┘ └─┘ └─┘
typ ┴ ┴ └─┘ ┴ └─┘ └─┘ └─┘ └─┘ ┴ └─┘ └─┘ └─┘ ┴ └─┘
382 λ s, by rcases s with ⟨_ | _⟩ | _; refl,
id ┴ ┴
src └─────┘ └───────────────┘ └──┘
typ ┴ └─────┘┴└───────────────┘ └──┘
doc └─────┘ └───────────────┘ └──┘
txt └─────┘ └───────────────┘ └──┘
par └─────┘ └───────────────┘ └──┘
pid ┴ └───────────────┘
st └──────────────────────────────┘
383 λ s, by rcases s with _ | _ | _; refl⟩
id ┴ ┴
src └─────┘ └─────────────┘ └──┘
typ ┴ └─────┘┴└─────────────┘ └──┘
doc └─────┘ └─────────────┘ └──┘
txt └─────┘ └─────────────┘ └──┘
par └─────┘ └─────────────┘ └──┘
pid ┴ └─────────────┘
st └────────────────────────────┘
384
385 @[simp] theorem sum_assoc_apply_in1 {α β γ} (a) : sum_assoc α β γ (inl (inl a)) = inl a := rfl
id └───────┘ ┴ ┴ ┴ └─┘ └─┘ ┴ ┴ └─┘ ┴ └─┘
src └───────┘ └─┘ └─┘ ┴ └─┘ └─┘
typ └───────┘ ┴ ┴ ┴ └─┘ └─┘ ┴ ┴ └─┘ ┴ └─┘
doc └──┘
386 @[simp] theorem sum_assoc_apply_in2 {α β γ} (b) : sum_assoc α β γ (inl (inr b)) = inr (inl b) := rfl
id └───────┘ ┴ ┴ ┴ └─┘ └─┘ ┴ ┴ └─┘ └─┘ ┴ └─┘
src └───────┘ └─┘ └─┘ ┴ └─┘ └─┘ └─┘
typ └───────┘ ┴ ┴ ┴ └─┘ └─┘ ┴ ┴ └─┘ └─┘ ┴ └─┘
doc └──┘
387 @[simp] theorem sum_assoc_apply_in3 {α β γ} (c) : sum_assoc α β γ (inr c) = inr (inr c) := rfl
id └───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ └─┘ ┴ └─┘
src └───────┘ └─┘ ┴ └─┘ └─┘ └─┘
typ └───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ └─┘ ┴ └─┘
doc └──┘
388
389 @[simp] def sum_empty (α : Sort*) : α ⊕ empty ≃ α :=
id ┴ ┴ └───┘ ┴ ┴
src ┴ └───┘ ┴
typ ┴ ┴ └───┘ ┴ ┴
doc └──┘ ┴
390 ⟨λ s, match s with inl a := a | inr e := empty.rec _ e end,
id ┴ ┴ └─┘ ┴ └─┘ ┴ └───────┘
src └─┘ └─┘ └───────┘
typ ┴ ┴ └─┘ ┴ └─┘ ┴ └───────┘
391 inl,
id └─┘
src └─┘
typ └─┘
392 λ s, by { rcases s with _ | ⟨⟨⟩⟩, refl },
id ┴ ┴
src └─────┘ └────────────┘ └───┘
typ ┴ └─────┘┴└────────────┘ └───┘
doc └─────┘ └────────────┘ └───┘
txt └─────┘ └────────────┘ └───┘
par └─────┘ └────────────┘ └───┘
pid ┴ └────────────┘ ┴
st └───────────────────────┘└─────┘└┘
393 λ a, rfl⟩
id ┴ └─┘
src └─┘
typ ┴ └─┘
394
395 @[simp] def empty_sum (α : Sort*) : empty ⊕ α ≃ α :=
id └───┘ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴
doc └──┘ ┴
396 (sum_comm _ _).trans $ sum_empty _
id └──────┘ └───┘ └───────┘
src └──────┘ └───┘ └───────┘
typ └──────┘ └───┘ └───────┘
397
398 @[simp] def sum_pempty (α : Sort*) : α ⊕ pempty ≃ α :=
id ┴ ┴ └────┘ ┴ ┴
src ┴ └────┘ ┴
typ ┴ ┴ └────┘ ┴ ┴
doc └──┘ └────┘ ┴
399 ⟨λ s, match s with inl a := a | inr e := pempty.rec _ e end,
id ┴ ┴ └─┘ ┴ └─┘ ┴ └────────┘
src └─┘ └─┘ └────────┘
typ ┴ ┴ └─┘ ┴ └─┘ ┴ └────────┘
400 inl,
id └─┘
src └─┘
typ └─┘
401 λ s, by { rcases s with _ | ⟨⟨⟩⟩, refl },
id ┴ ┴
src └─────┘ └────────────┘ └───┘
typ ┴ └─────┘┴└────────────┘ └───┘
doc └─────┘ └────────────┘ └───┘
txt └─────┘ └────────────┘ └───┘
par └─────┘ └────────────┘ └───┘
pid ┴ └────────────┘ ┴
st └───────────────────────┘└─────┘└┘
402 λ a, rfl⟩
id ┴ └─┘
src └─┘
typ ┴ └─┘
403
404 @[simp] def pempty_sum (α : Sort*) : pempty ⊕ α ≃ α :=
id └────┘ ┴ ┴ ┴ ┴
src └────┘ ┴ ┴
typ └────┘ ┴ ┴ ┴ ┴
doc └──┘ └────┘ ┴
405 (sum_comm _ _).trans $ sum_pempty _
id └──────┘ └───┘ └────────┘
src └──────┘ └───┘ └────────┘
typ └──────┘ └───┘ └────────┘
406
407 @[simp] def option_equiv_sum_punit (α : Sort*) : option α ≃ α ⊕ punit.{u+1} :=
id └────┘ ┴ ┴ ┴ ┴ └───┘
src └────┘ ┴ ┴ └───┘
typ └────┘ ┴ ┴ ┴ ┴ └───┘
doc └──┘ ┴
408 ⟨λ o, match o with none := inr punit.star | some a := inl a end,
id ┴ ┴ └──┘ └─┘ └────────┘ └──┘ ┴ └─┘
src └──┘ └─┘ └────────┘ └──┘ └─┘
typ ┴ ┴ └──┘ └─┘ └────────┘ └──┘ ┴ └─┘
409 λ s, match s with inr _ := none | inl a := some a end,
id ┴ ┴ └─┘ └──┘ └─┘ ┴ └──┘
src └─┘ └──┘ └─┘ └──┘
typ ┴ ┴ └─┘ └──┘ └─┘ ┴ └──┘
410 λ o, by cases o; refl,
id ┴ ┴
src └────┘ └──┘
typ ┴ └────┘┴ └──┘
doc └────┘ └──┘
txt └────┘ └──┘
par └────┘ └──┘
pid ┴
st └────────────┘
411 λ s, by rcases s with _ | ⟨⟨⟩⟩; refl⟩
id ┴ ┴
src └─────┘ └────────────┘ └──┘
typ ┴ └─────┘┴└────────────┘ └──┘
doc └─────┘ └────────────┘ └──┘
txt └─────┘ └────────────┘ └──┘
par └─────┘ └────────────┘ └──┘
pid ┴ └────────────┘
st └───────────────────────────┘
412
413 def sum_equiv_sigma_bool (α β : Sort*) : α ⊕ β ≃ (Σ b: bool, cond b α β) :=
id ┴ ┴ ┴ ┴ ┴ └──┘┴ └──┘ ┴ ┴ ┴
src ┴ ┴ ┴ └──┘┴ └──┘
typ ┴ ┴ ┴ ┴ ┴ └──┘┴ └──┘ ┴ ┴ ┴
doc ┴
414 ⟨λ s, match s with inl a := ⟨tt, a⟩ | inr b := ⟨ff, b⟩ end,
id ┴ ┴ └─┘ ┴ └┘ └─┘ ┴ └┘
src └─┘ └┘ └─┘ └┘
typ ┴ ┴ └─┘ ┴ └┘ └─┘ ┴ └┘
415 λ s, match s with ⟨tt, a⟩ := inl a | ⟨ff, b⟩ := inr b end,
id ┴ ┴ └┘ ┴ └─┘ └┘ ┴ └─┘
src └┘ └─┘ └┘ └─┘
typ ┴ ┴ └┘ ┴ └─┘ └┘ ┴ └─┘
416 λ s, by cases s; refl,
id ┴ ┴
src └────┘ └──┘
typ ┴ └────┘┴ └──┘
doc └────┘ └──┘
txt └────┘ └──┘
par └────┘ └──┘
pid ┴
st └────────────┘
417 λ s, by rcases s with ⟨_|_, _⟩; refl⟩
id ┴ ┴
src └─────┘ └────────────┘ └──┘
typ ┴ └─────┘┴└────────────┘ └──┘
doc └─────┘ └────────────┘ └──┘
txt └─────┘ └────────────┘ └──┘
par └─────┘ └────────────┘ └──┘
pid ┴ └────────────┘
st └───────────────────────────┘
418
419 def sigma_preimage_equiv {α β : Type*} (f : α → β) :
id ┴ ┴
typ ┴ ┴
420 (Σ y : β, {x // f x = y}) ≃ α :=
id ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
421 ⟨λ x, x.2.1, λ x, ⟨f x, x, rfl⟩, λ ⟨y, x, rfl⟩, rfl, λ x, rfl⟩
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └─┘ └─┘ ┴ └─┘
src ┴ ┴ └─┘ └─┘ └─┘ └─┘
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └─┘ └─┘ ┴ └─┘
422
423 end
424
425 section
426
427 def Pi_congr_right {α} {β₁ β₂ : α → Sort*} (F : ∀ a, β₁ a ≃ β₂ a) : (Π a, β₁ a) ≃ (Π a, β₂ a) :=
id ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴
src ┴ ┴
typ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴
doc ┴ ┴
428 ⟨λ H a, F a (H a), λ H a, (F a).symm (H a),
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
src └──┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
429 λ H, funext $ by simp, λ H, funext $ by simp⟩
id ┴ └────┘ ┴ └────┘
src └────┘ └──┘ └────┘ └──┘
typ ┴ └────┘ └──┘ ┴ └────┘ └──┘
doc └──┘ └──┘
txt └──┘ └──┘
par └──┘ └──┘
st └───┘ └───┘
430
431 def Pi_curry {α} {β : α → Sort*} (γ : Π a, β a → Sort*) : (Π x : sigma β, γ x.1 x.2) ≃ (Π a b, γ a b) :=
id ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
432 { to_fun := λ f x y, f ⟨x,y⟩,
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
433 inv_fun := λ f x, f x.1 x.2,
id ┴ ┴ ┴ ┴┴ ┴┴
src ┴ ┴
typ ┴ ┴ ┴ ┴┴ ┴┴
434 left_inv := λ f, funext $ λ ⟨x,y⟩, rfl,
id ┴ └────┘ ┴ └─┘
src └────┘ └─┘
typ ┴ └────┘ ┴ └─┘
435 right_inv := λ f, funext $ λ x, funext $ λ y, rfl }
id ┴ └────┘ ┴ └────┘ ┴ └─┘
src └────┘ └────┘ └─┘
typ ┴ └────┘ ┴ └────┘ ┴ └─┘
436
437 end
438
439 section
440 def psigma_equiv_sigma {α} (β : α → Sort*) : psigma β ≃ sigma β :=
id ┴ └────┘ ┴ ┴ └───┘ ┴
src └────┘ ┴ └───┘
typ ┴ └────┘ ┴ ┴ └───┘ ┴
doc ┴
441 ⟨λ ⟨a, b⟩, ⟨a, b⟩, λ ⟨a, b⟩, ⟨a, b⟩, λ ⟨a, b⟩, rfl, λ ⟨a, b⟩, rfl⟩
id ┴┴ ┴ ┴┴ ┴ ┴ └─┘ ┴ └─┘
src └─┘ └─┘
typ ┴┴ ┴ ┴┴ ┴ ┴ └─┘ ┴ └─┘
442
443 def sigma_congr_right {α} {β₁ β₂ : α → Sort*} (F : ∀ a, β₁ a ≃ β₂ a) : sigma β₁ ≃ sigma β₂ :=
id ┴ ┴ └┘ ┴ ┴ └┘ ┴ └───┘ └┘ ┴ └───┘ └┘
src ┴ └───┘ ┴ └───┘
typ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └───┘ └┘ ┴ └───┘ └┘
doc ┴ ┴
444 ⟨λ ⟨a, b⟩, ⟨a, F a b⟩, λ ⟨a, b⟩, ⟨a, (F a).symm b⟩,
id ┴┴ ┴ ┴ ┴┴ ┴ ┴ └──┘
src └──┘
typ ┴┴ ┴ ┴ ┴┴ ┴ ┴ └──┘
445 λ ⟨a, b⟩, congr_arg (sigma.mk a) $ symm_apply_apply (F a) b,
id ┴┴ ┴ └───────┘ └──────┘ └──────────────┘ ┴
src └───────┘ └──────┘ └──────────────┘
typ ┴┴ ┴ └───────┘ └──────┘ └──────────────┘ ┴
446 λ ⟨a, b⟩, congr_arg (sigma.mk a) $ apply_symm_apply (F a) b⟩
id ┴┴ ┴ └───────┘ └──────┘ └──────────────┘ ┴
src └───────┘ └──────┘ └──────────────┘
typ ┴┴ ┴ └───────┘ └──────┘ └──────────────┘ ┴
447
448 def sigma_congr_left {α₁ α₂} {β : α₂ → Sort*} : ∀ f : α₁ ≃ α₂, (Σ a:α₁, β (f a)) ≃ (Σ a:α₂, β a)
id └┘ ┴ └┘ ┴ └┘ ┴ └┘┴ ┴ ┴ ┴ ┴ ┴ └┘┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ └┘ ┴ └┘ ┴ └┘ ┴ └┘┴ ┴ ┴ ┴ ┴ ┴ └┘┴ ┴ ┴
doc ┴ ┴
449 | ⟨f, g, l, r⟩ :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
450 ⟨λ ⟨a, b⟩, ⟨f a, b⟩, λ ⟨a, b⟩, ⟨g a, @@eq.rec β b (r a).symm⟩,
id ┴┴ ┴ ┴┴ ┴ └────┘ ┴ └──┘
src └────┘ └──┘
typ ┴┴ ┴ ┴┴ ┴ └────┘ ┴ └──┘
451 λ ⟨a, b⟩, match g (f a), l a : ∀ a' (h : a' = a),
id ┴┴ ┴ └┘ ┴
src ┴
typ ┴┴ ┴ └┘ ┴
452 @sigma.mk _ (β ∘ f) _ (@@eq.rec β b (congr_arg f h.symm)) = ⟨a, b⟩ with
id └──────┘ ┴ ┴ └────┘ ┴ └───────┘ ┴└───┘ ┴
src └──────┘ ┴ └────┘ └───────┘ └───┘ ┴
typ └──────┘ ┴ ┴ └────┘ ┴ └───────┘ ┴└───┘ ┴
453 | _, rfl := rfl end,
id └─┘ └─┘
src └─┘ └─┘
typ └─┘ └─┘
454 λ ⟨a, b⟩, match f (g a), _ : ∀ a' (h : a' = a), sigma.mk a' (@@eq.rec β b h.symm) = ⟨a, b⟩ with
id ┴┴ ┴ └┘ ┴ └──────┘ └┘ └────┘ ┴ ┴└───┘ ┴
src ┴ └──────┘ └────┘ └───┘ ┴
typ ┴┴ ┴ └┘ ┴ └──────┘ └┘ └────┘ ┴ ┴└───┘ ┴
455 | _, rfl := rfl end⟩
id └─┘ └─┘
src └─┘ └─┘
typ └─┘ └─┘
456
457 def sigma_equiv_prod (α β : Sort*) : (Σ_:α, β) ≃ α × β :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
doc ┴
458 ⟨λ ⟨a, b⟩, ⟨a, b⟩, λ ⟨a, b⟩, ⟨a, b⟩, λ ⟨a, b⟩, rfl, λ ⟨a, b⟩, rfl⟩
id ┴┴ ┴ ┴┴ ┴ ┴ └─┘ ┴ └─┘
src └─┘ └─┘
typ ┴┴ ┴ ┴┴ ┴ ┴ └─┘ ┴ └─┘
459
460 def sigma_equiv_prod_of_equiv {α β} {β₁ : α → Sort*} (F : ∀ a, β₁ a ≃ β) : sigma β₁ ≃ α × β :=
id ┴ ┴ └┘ ┴ ┴ ┴ └───┘ └┘ ┴ ┴ ┴ ┴
src ┴ └───┘ ┴ ┴
typ ┴ ┴ └┘ ┴ ┴ ┴ └───┘ └┘ ┴ ┴ ┴ ┴
doc ┴ ┴
461 (sigma_congr_right F).trans (sigma_equiv_prod α β)
id └───────────────┘ ┴ └───┘ └──────────────┘ ┴ ┴
src └───────────────┘ └───┘ └──────────────┘
typ └───────────────┘ ┴ └───┘ └──────────────┘ ┴ ┴
462
463 end
464
465 section
466 def arrow_prod_equiv_prod_arrow (α β γ : Type*) : (γ → α × β) ≃ (γ → α) × (γ → β) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
467 ⟨λ f, (λ c, (f c).1, λ c, (f c).2),
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
468 λ p c, (p.1 c, p.2 c),
id ┴ ┴ ┴┴┴ ┴ ┴┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴┴┴ ┴ ┴┴ ┴
469 λ f, funext $ λ c, prod.mk.eta,
id ┴ └────┘ ┴ └─────────┘
src └────┘ └─────────┘
typ ┴ └────┘ ┴ └─────────┘
470 λ p, by { cases p, refl }⟩
id ┴ ┴
src └────┘ └───┘
typ ┴ └────┘┴ └───┘
doc └────┘ └───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴ ┴
st └────────┘└─────┘└┘
471
472 def arrow_arrow_equiv_prod_arrow (α β γ : Sort*) : (α → β → γ) ≃ (α × β → γ) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
473 ⟨λ f, λ p, f p.1 p.2,
id ┴ ┴ ┴ ┴┴ ┴┴
src ┴ ┴
typ ┴ ┴ ┴ ┴┴ ┴┴
474 λ f, λ a b, f (a, b),
id ┴ ┴ ┴ ┴ ┴┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴┴ ┴
475 λ f, rfl,
id ┴ └─┘
src └─┘
typ ┴ └─┘
476 λ f, by { funext p, cases p, refl }⟩
id ┴ ┴
src └──────┘ └────┘ └───┘
typ ┴ └──────┘ └────┘┴ └───┘
doc └──────┘ └────┘ └───┘
txt └──────┘ └────┘ └───┘
par └──────┘ └────┘ └───┘
pid └┘ ┴ ┴
st └─────────┘└───────┘└─────┘└┘
477
478 open sum
479 def sum_arrow_equiv_prod_arrow (α β γ : Type*) : ((α ⊕ β) → γ) ≃ (α → γ) × (β → γ) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
480 ⟨λ f, (f ∘ inl, f ∘ inr),
id ┴ ┴┴ ┴ └─┘ ┴ ┴ └─┘
src ┴ ┴ └─┘ ┴ └─┘
typ ┴ ┴┴ ┴ └─┘ ┴ ┴ └─┘
481 λ p s, sum.rec_on s p.1 p.2,
id ┴ ┴ └────────┘ ┴ ┴┴ ┴┴
src └────────┘ ┴ ┴
typ ┴ ┴ └────────┘ ┴ ┴┴ ┴┴
482 λ f, by { funext s, cases s; refl },
id ┴ ┴
src └──────┘ └────┘ └───┘
typ ┴ └──────┘ └────┘┴ └───┘
doc └──────┘ └────┘ └───┘
txt └──────┘ └────┘ └───┘
par └──────┘ └────┘ └───┘
pid └┘ ┴ ┴
st └─────────┘└──────────────┘└┘
483 λ p, by { cases p, refl }⟩
id ┴ ┴
src └────┘ └───┘
typ ┴ └────┘┴ └───┘
doc └────┘ └───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴ ┴
st └────────┘└─────┘└┘
484
485 def sum_prod_distrib (α β γ : Sort*) : (α ⊕ β) × γ ≃ (α × γ) ⊕ (β × γ) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
486 ⟨λ p, match p with (inl a, c) := inl (a, c) | (inr b, c) := inr (b, c) end,
id ┴ ┴ ┴└─┘ ┴ ┴ └─┘ ┴ ┴└─┘ ┴ ┴ └─┘ ┴
src ┴└─┘ └─┘ ┴ ┴└─┘ └─┘ ┴
typ ┴ ┴ ┴└─┘ ┴ ┴ └─┘ ┴ ┴└─┘ ┴ ┴ └─┘ ┴
487 λ s, match s with inl (a, c) := (inl a, c) | inr (b, c) := (inr b, c) end,
id ┴ ┴ └─┘ ┴┴ ┴ ┴└─┘ └─┘ ┴┴ ┴ ┴└─┘
src └─┘ ┴ ┴└─┘ └─┘ ┴ ┴└─┘
typ ┴ ┴ └─┘ ┴┴ ┴ ┴└─┘ └─┘ ┴┴ ┴ ┴└─┘
488 λ p, by rcases p with ⟨_ | _, _⟩; refl,
id ┴ ┴
src └─────┘ └──────────────┘ └──┘
typ ┴ └─────┘┴└──────────────┘ └──┘
doc └─────┘ └──────────────┘ └──┘
txt └─────┘ └──────────────┘ └──┘
par └─────┘ └──────────────┘ └──┘
pid ┴ └──────────────┘
st └─────────────────────────────┘
489 λ s, by rcases s with ⟨_, _⟩ | ⟨_, _⟩; refl⟩
id ┴ ┴
src └─────┘ └───────────────────┘ └──┘
typ ┴ └─────┘┴└───────────────────┘ └──┘
doc └─────┘ └───────────────────┘ └──┘
txt └─────┘ └───────────────────┘ └──┘
par └─────┘ └───────────────────┘ └──┘
pid ┴ └───────────────────┘
st └──────────────────────────────────┘
490
491 @[simp] theorem sum_prod_distrib_apply_left {α β γ} (a : α) (c : γ) :
id ┴ ┴
typ ┴ ┴
doc └──┘
492 sum_prod_distrib α β γ (sum.inl a, c) = sum.inl (a, c) := rfl
id └──────────────┘ ┴ ┴ ┴ ┴└─────┘ ┴ ┴ ┴ └─────┘ ┴┴ ┴ └─┘
src └──────────────┘ ┴└─────┘ ┴ └─────┘ ┴ └─┘
typ └──────────────┘ ┴ ┴ ┴ ┴└─────┘ ┴ ┴ ┴ └─────┘ ┴┴ ┴ └─┘
493 @[simp] theorem sum_prod_distrib_apply_right {α β γ} (b : β) (c : γ) :
id ┴ ┴
typ ┴ ┴
doc └──┘
494 sum_prod_distrib α β γ (sum.inr b, c) = sum.inr (b, c) := rfl
id └──────────────┘ ┴ ┴ ┴ ┴└─────┘ ┴ ┴ ┴ └─────┘ ┴┴ ┴ └─┘
src └──────────────┘ ┴└─────┘ ┴ └─────┘ ┴ └─┘
typ └──────────────┘ ┴ ┴ ┴ ┴└─────┘ ┴ ┴ ┴ └─────┘ ┴┴ ┴ └─┘
495
496 def prod_sum_distrib (α β γ : Sort*) : α × (β ⊕ γ) ≃ (α × β) ⊕ (α × γ) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
497 calc α × (β ⊕ γ) ≃ (β ⊕ γ) × α : prod_comm _ _
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘
src ┴ ┴ ┴ ┴ └───────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘
498 ... ≃ (β × α) ⊕ (γ × α) : sum_prod_distrib _ _ _
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────────────┘
src ┴ ┴ ┴ └──────────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────────────┘
499 ... ≃ (α × β) ⊕ (α × γ) : sum_congr (prod_comm _ _) (prod_comm _ _)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ └───────┘ └───────┘
src ┴ ┴ ┴ └───────┘ └───────┘ └───────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ └───────┘ └───────┘
500
501 @[simp] theorem prod_sum_distrib_apply_left {α β γ} (a : α) (b : β) :
id ┴ ┴
typ ┴ ┴
doc └──┘
502 prod_sum_distrib α β γ (a, sum.inl b) = sum.inl (a, b) := rfl
id └──────────────┘ ┴ ┴ ┴ ┴┴ └─────┘ ┴ ┴ └─────┘ ┴┴ ┴ └─┘
src └──────────────┘ ┴ └─────┘ ┴ └─────┘ ┴ └─┘
typ └──────────────┘ ┴ ┴ ┴ ┴┴ └─────┘ ┴ ┴ └─────┘ ┴┴ ┴ └─┘
503 @[simp] theorem prod_sum_distrib_apply_right {α β γ} (a : α) (c : γ) :
id ┴ ┴
typ ┴ ┴
doc └──┘
504 prod_sum_distrib α β γ (a, sum.inr c) = sum.inr (a, c) := rfl
id └──────────────┘ ┴ ┴ ┴ ┴┴ └─────┘ ┴ ┴ └─────┘ ┴┴ ┴ └─┘
src └──────────────┘ ┴ └─────┘ ┴ └─────┘ ┴ └─┘
typ └──────────────┘ ┴ ┴ ┴ ┴┴ └─────┘ ┴ ┴ └─────┘ ┴┴ ┴ └─┘
505
506 def sigma_prod_distrib {ι : Type*} (α : ι → Type*) (β : Type*) :
id ┴
typ ┴
507 ((Σ i, α i) × β) ≃ (Σ i, (α i × β)) :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc ┴
508 ⟨λ p, ⟨p.1.1, (p.1.2, p.2)⟩,
id ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴
509 λ p, (⟨p.1, p.2.1⟩, p.2.2),
id ┴ ┴ ┴┴ ┴┴ ┴ ┴┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴┴ ┴ ┴┴ ┴
510 λ p, by { rcases p with ⟨⟨_, _⟩, _⟩, refl },
id ┴ ┴
src └─────┘ └───────────────┘ └───┘
typ ┴ └─────┘┴└───────────────┘ └───┘
doc └─────┘ └───────────────┘ └───┘
txt └─────┘ └───────────────┘ └───┘
par └─────┘ └───────────────┘ └───┘
pid ┴ └───────────────┘ ┴
st └──────────────────────────┘└─────┘└┘
511 λ p, by { rcases p with ⟨_, ⟨_, _⟩⟩, refl }⟩
id ┴ ┴
src └─────┘ └───────────────┘ └───┘
typ ┴ └─────┘┴└───────────────┘ └───┘
doc └─────┘ └───────────────┘ └───┘
txt └─────┘ └───────────────┘ └───┘
par └─────┘ └───────────────┘ └───┘
pid ┴ └───────────────┘ ┴
st └──────────────────────────┘└─────┘└┘
512
513 def bool_prod_equiv_sum (α : Type u) : bool × α ≃ α ⊕ α :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
514 calc bool × α ≃ (unit ⊕ unit) × α : prod_congr bool_equiv_punit_sum_punit (equiv.refl _)
id └──┘ ┴ ┴ └──┘ ┴ └──┘ ┴ ┴ └────────┘ └────────────────────────┘ └────────┘
src └──┘ ┴ └──┘ ┴ └──┘ ┴ └────────┘ └────────────────────────┘ └────────┘
typ └──┘ ┴ ┴ └──┘ ┴ └──┘ ┴ ┴ └────────┘ └────────────────────────┘ └────────┘
doc └──┘ └──┘
515 ... ≃ α × (unit ⊕ unit) : prod_comm _ _
id ┴ ┴ └──┘ ┴ └──┘ └───────┘
src ┴ └──┘ ┴ └──┘ └───────┘
typ ┴ ┴ └──┘ ┴ └──┘ └───────┘
doc └──┘ └──┘
516 ... ≃ (α × unit) ⊕ (α × unit) : prod_sum_distrib _ _ _
id ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ └──────────────┘
src ┴ └──┘ ┴ ┴ └──┘ └──────────────┘
typ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ └──────────────┘
doc └──┘ └──┘
517 ... ≃ α ⊕ α : sum_congr (prod_punit _) (prod_punit _)
id ┴ ┴ ┴ └───────┘ └────────┘ └────────┘
src ┴ └───────┘ └────────┘ └────────┘
typ ┴ ┴ ┴ └───────┘ └────────┘ └────────┘
518 end
519
520 section
521 open sum nat
522 def nat_equiv_nat_sum_punit : ℕ ≃ ℕ ⊕ punit.{u+1} :=
id ┴ ┴ ┴ ┴ └───┘
src ┴ ┴ ┴ ┴ └───┘
typ ┴ ┴ ┴ ┴ └───┘
doc ┴
523 ⟨λ n, match n with zero := inr punit.star | succ a := inl a end,
id ┴ ┴ └──┘ └─┘ └────────┘ └──┘ ┴ └─┘
src └──┘ └─┘ └────────┘ └──┘ └─┘
typ ┴ ┴ └──┘ └─┘ └────────┘ └──┘ ┴ └─┘
524 λ s, match s with inl n := succ n | inr punit.star := zero end,
id ┴ ┴ └─┘ ┴ └──┘ └─┘ └────────┘ └──┘
src └─┘ └──┘ └─┘ └────────┘ └──┘
typ ┴ ┴ └─┘ ┴ └──┘ └─┘ └────────┘ └──┘
525 λ n, begin cases n, repeat { refl } end,
id ┴ ┴
src └────┘ └───────┘└───┘└┘
typ ┴ └────┘┴ └───────┘└───┘└┘
doc └────┘ └───────┘└───┘└┘
txt └────┘ └───────┘└───┘└┘
par └────┘ └───────┘└───┘└┘
pid ┴ └───────┘┴
st └───────────┘└────────┘└────┘┴┴└─┘
526 λ s, begin cases s with a u, { refl }, {cases u, { refl }} end⟩
id ┴ ┴ ┴
src └────┘ └───────┘ └───┘ └────┘ └───┘
typ ┴ └────┘┴└───────┘ └───┘ └────┘┴ └───┘
doc └────┘ └───────┘ └───┘ └────┘ └───┘
txt └────┘ └───────┘ └───┘ └────┘ └───┘
par └────┘ └───────┘ └───┘ └────┘ └───┘
pid ┴ └───────┘ ┴ ┴ ┴
st └────────────────────┘└──┘└───┘└┘└───────┘└───────┘└────┘
527
528 @[simp] def nat_sum_punit_equiv_nat : ℕ ⊕ punit.{u+1} ≃ ℕ :=
id ┴ ┴ └───┘ ┴ ┴
src ┴ ┴ └───┘ ┴ ┴
typ ┴ ┴ └───┘ ┴ ┴
doc └──┘ ┴
529 nat_equiv_nat_sum_punit.symm
id └─────────────────────┘└───┘
src └─────────────────────┘└───┘
typ └─────────────────────┘└───┘
530
531 def int_equiv_nat_sum_nat : ℤ ≃ ℕ ⊕ ℕ :=
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
doc ┴
532 by refine ⟨_, _, _, _⟩; intro z; {cases z; [left, right]; assumption} <|> {cases z; refl}
id ┴ ┴ ┴
src └─────┘ └─────────┘ └─────┘ └────┘ ┴└──┘ └───┘ └────────┘ └────┘ └──┘
typ └─────┘ └─────────┘ └─────┘ └────┘┴ ┴└──┘ └───┘ └────────┘ └────┘┴ └──┘
doc └─────┘ └─────────┘ └─────┘ └────┘ └──┘ └───┘ └────────┘ └────┘ └──┘
txt └─────┘ └─────────┘ └─────┘ └────┘ └──┘ └───┘ └────────┘ └────┘ └──┘
par └─────┘ └─────────┘ └─────┘ └────┘ └──┘ └───┘ └────────┘ └────┘ └──┘
pid ┴ └─────────┘ └┘ ┴ ┴
st └─────────────────────────────┘└─────────────────────────────────┘└┘└──┘└────────────┘└┘
533
534 end
535
536 def list_equiv_of_equiv {α β : Type*} : α ≃ β → list α ≃ list β
id ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
src ┴ └──┘ ┴ └──┘
typ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
doc ┴ ┴
537 | ⟨f, g, l, r⟩ :=
538 by refine ⟨list.map f, list.map g, λ x, _, λ x, _⟩;
id ┴ └──────┘ ┴
src └─────┘ ┴ └┘└──────┘┴ └┘ └─────┘ └────┘
typ └─────┘ ┴┴└┘└──────┘┴┴└┘ └─────┘ └────┘
doc └─────┘ ┴ └┘ ┴ └┘ └─────┘ └────┘
txt └─────┘ ┴ └┘ ┴ └┘ └─────┘ └────┘
par └─────┘ ┴ └┘ ┴ └┘ └─────┘ └────┘
pid ┴ ┴ └┘ ┴ └┘ └─────┘ └────┘
st └─────────────────────────────────────────────────
539 simp [id_of_left_inverse l, id_of_right_inverse r]
id └────────────────┘ ┴ └─────────────────┘ ┴
src └────┘└────────────────┘┴ └┘└─────────────────┘┴ └─
typ └────┘└────────────────┘┴┴└┘└─────────────────┘┴┴└─
doc └────┘ ┴ └┘ ┴ └─
txt └────┘ ┴ └┘ ┴ └─
par └────┘ ┴ └┘ ┴ └─
pid ┴┴ ┴ └┘ ┴ ┴└
st ────────────────────────────────────────────────────────
540
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
541 def fin_equiv_subtype (n : ℕ) : fin n ≃ {m // m < n} :=
id ┴ └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴
src ┴ └─┘ ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴
doc ┴
542 ⟨λ x, ⟨x.1, x.2⟩, λ x, ⟨x.1, x.2⟩, λ ⟨a, b⟩, rfl,λ ⟨a, b⟩, rfl⟩
id ┴ ┴┴ ┴┴ ┴ ┴┴ ┴┴ ┴ └─┘ ┴ └─┘
src ┴ ┴ ┴ ┴ └─┘ └─┘
typ ┴ ┴┴ ┴┴ ┴ ┴┴ ┴┴ ┴ └─┘ ┴ └─┘
543
544 def decidable_eq_of_equiv [decidable_eq β] (e : α ≃ β) : decidable_eq α
id └──────────┘ ┴ ┴ ┴ ┴ └──────────┘ ┴
src └──────────┘ ┴ └──────────┘
typ └──────────┘ ┴ ┴ ┴ ┴ └──────────┘ ┴
doc ┴
545 | a₁ a₂ := decidable_of_iff (e a₁ = e a₂) e.injective.eq_iff
id └┘ └┘ └──────────────┘ ┴ ┴ ┴ ┴└────────┘└─────┘
src └──────────────┘ ┴ └────────┘└─────┘
typ └┘ └┘ └──────────────┘ ┴ ┴ ┴ ┴└────────┘└─────┘
546
547 def inhabited_of_equiv [inhabited β] (e : α ≃ β) : inhabited α :=
id └───────┘ ┴ ┴ ┴ ┴ └───────┘ ┴
src └───────┘ ┴ └───────┘
typ └───────┘ ┴ ┴ ┴ ┴ └───────┘ ┴
doc ┴
548 ⟨e.symm (default _)⟩
id ┴└───┘ └─────┘
src └───┘ └─────┘
typ ┴└───┘ └─────┘
549
550 def unique_of_equiv (e : α ≃ β) (h : unique β) : unique α :=
id ┴ ┴ ┴ └────┘ ┴ └────┘ ┴
src ┴ └────┘ └────┘
typ ┴ ┴ ┴ └────┘ ┴ └────┘ ┴
doc ┴
551 unique.of_surjective e.symm.surjective
id └──────────────────┘ ┴└───┘└─────────┘
src └──────────────────┘ └───┘└─────────┘
typ └──────────────────┘ ┴└───┘└─────────┘
552
553 def unique_congr (e : α ≃ β) : unique α ≃ unique β :=
id ┴ ┴ ┴ └────┘ ┴ ┴ └────┘ ┴
src ┴ └────┘ ┴ └────┘
typ ┴ ┴ ┴ └────┘ ┴ ┴ └────┘ ┴
doc ┴ ┴
554 { to_fun := e.symm.unique_of_equiv,
id ┴└───┘└──────────────┘
src └───┘└──────────────┘
typ ┴└───┘└──────────────┘
555 inv_fun := e.unique_of_equiv,
id ┴└──────────────┘
src └──────────────┘
typ ┴└──────────────┘
556 left_inv := λ _, subsingleton.elim _ _,
id ┴ └───────────────┘
src └───────────────┘
typ ┴ └───────────────┘
557 right_inv := λ _, subsingleton.elim _ _ }
id ┴ └───────────────┘
src └───────────────┘
typ ┴ └───────────────┘
558
559 section
560 open subtype
561
562 def subtype_congr {p : α → Prop} {q : β → Prop}
id ┴ ┴
typ ┴ ┴
563 (e : α ≃ β) (h : ∀ a, p a ↔ q (e a)) : {a : α // p a} ≃ {b : β // q b} :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴
564 ⟨λ x, ⟨e x.1, (h _).1 x.2⟩,
id ┴ ┴ ┴┴ ┴ ┴ ┴┴
src ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴ ┴┴
565 λ y, ⟨e.symm y.1, (h _).2 (by { simp, exact y.2 })⟩,
id ┴ ┴└───┘ ┴┴ ┴ ┴ ┴
src └───┘ ┴ ┴ └──┘ └────┘ └─┘
typ ┴ ┴└───┘ ┴┴ ┴ ┴ └──┘ └────┘┴└─┘
doc └──┘ └────┘ └─┘
txt └──┘ └────┘ └─┘
par └──┘ └────┘ └─┘
pid ┴ └─┘
st └─────┘└──────────┘└┘
566 λ ⟨x, h⟩, subtype.eq' $ by simp,
id ┴ └─────────┘
src └─────────┘ └──┘
typ ┴ └─────────┘ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
567 λ ⟨y, h⟩, subtype.eq' $ by simp⟩
id ┴ └─────────┘
src └─────────┘ └──┘
typ ┴ └─────────┘ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
568
569 def subtype_congr_right {p q : α → Prop} (e : ∀x, p x ↔ q x) : subtype p ≃ subtype q :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴
src ┴ └─────┘ ┴ └─────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴
doc ┴
570 subtype_congr (equiv.refl _) e
id └───────────┘ └────────┘ ┴
src └───────────┘ └────────┘
typ └───────────┘ └────────┘ ┴
571
572 @[simp] lemma subtype_congr_right_mk {p q : α → Prop} (e : ∀x, p x ↔ q x)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
573 {x : α} (h : p x) : subtype_congr_right e ⟨x, h⟩ = ⟨x, (e x).1 h⟩ := rfl
id ┴ ┴ ┴ └─────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
src └─────────────────┘ ┴ ┴ └─┘
typ ┴ ┴ ┴ └─────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
574
575 def subtype_equiv_of_subtype' {p : α → Prop} (e : α ≃ β) :
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
doc ┴
576 {a : α // p a} ≃ {b : β // p (e.symm b)} :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘ ┴
src ┴ ┴ ┴ └───┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘ ┴
doc ┴
577 subtype_congr e $ by simp
id └───────────┘ ┴
src └───────────┘ └────
typ └───────────┘ ┴ └────
doc └────
txt └────
par └────
pid └
st └─────
578
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
579 def subtype_congr_prop {α : Type*} {p q : α → Prop} (h : p = q) : subtype p ≃ subtype q :=
id ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴
src ┴ └─────┘ ┴ └─────┘
typ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴
doc ┴
580 subtype_congr (equiv.refl α) (assume a, h ▸ iff.rfl)
id └───────────┘ └────────┘ ┴ ┴ ┴ ┴ └─────┘
src └───────────┘ └────────┘ ┴ └─────┘
typ └───────────┘ └────────┘ ┴ ┴ ┴ ┴ └─────┘
581
582 def set_congr {α : Type*} {s t : set α} (h : s = t) : s ≃ t :=
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
583 subtype_congr_prop h
id └────────────────┘ ┴
src └────────────────┘
typ └────────────────┘ ┴
584
585 def subtype_subtype_equiv_subtype_exists {α : Type u} (p : α → Prop) (q : subtype p → Prop) :
id ┴ └─────┘ ┴
src └─────┘
typ ┴ └─────┘ ┴
586 subtype q ≃ {a : α // ∃h:p a, q ⟨a, h⟩ } :=
id └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ ┴ ┴
typ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
doc ┴
587 ⟨λ⟨⟨a, ha⟩, ha'⟩, ⟨a, ha, ha'⟩,
id ┴ ┴ └┘ └─┘
typ ┴ ┴ └┘ └─┘
588 λ⟨a, ha⟩, ⟨⟨a, ha.cases_on $ assume h _, h⟩, by { cases ha, exact ha_h }⟩,
id ┴┴ └┘ └───────┘ ┴ ┴ ┴ └┘ └──┘
src └───────┘ └────┘ └────┘ ┴
typ ┴┴ └┘ └───────┘ ┴ ┴ ┴ └────┘└┘ └────┘└──┘┴
doc └────┘ └────┘ ┴
txt └────┘ └────┘ ┴
par └────┘ └────┘ ┴
pid ┴ ┴ ┴
st └─────────┘└───────────┘└┘
589 assume ⟨⟨a, ha⟩, h⟩, rfl, assume ⟨a, h₁, h₂⟩, rfl⟩
id ┴ └─┘ ┴ └─┘
src └─┘ └─┘
typ ┴ └─┘ ┴ └─┘
590
591 def subtype_subtype_equiv_subtype_inter {α : Type u} (p q : α → Prop) :
id ┴
typ ┴
592 {x : subtype p // q x.1} ≃ subtype (λ x, p x ∧ q x) :=
id ┴ └─────┘ ┴ ┴ ┴┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └─────┘ ┴ ┴ └─────┘ ┴
typ ┴ └─────┘ ┴ ┴ ┴┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
593 (subtype_subtype_equiv_subtype_exists p _).trans $
id └──────────────────────────────────┘ ┴ └───┘
src └──────────────────────────────────┘ └───┘
typ └──────────────────────────────────┘ ┴ └───┘
594 subtype_congr_right $ λ x, exists_prop
id └─────────────────┘ ┴ └─────────┘
src └─────────────────┘ └─────────┘
typ └─────────────────┘ ┴ └─────────┘
595
596 /-- If the outer subtype has more restrictive predicate than the inner one,
597 then we can drop the latter. -/
598 def subtype_subtype_equiv_subtype {α : Type u} {p q : α → Prop} (h : ∀ {x}, q x → p x) :
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
599 {x : subtype p // q x.1} ≃ subtype q :=
id ┴ └─────┘ ┴ ┴ ┴┴ ┴ └─────┘ ┴
src ┴ └─────┘ ┴ ┴ └─────┘
typ ┴ └─────┘ ┴ ┴ ┴┴ ┴ └─────┘ ┴
doc ┴
600 (subtype_subtype_equiv_subtype_inter p _).trans $
id └─────────────────────────────────┘ ┴ └───┘
src └─────────────────────────────────┘ └───┘
typ └─────────────────────────────────┘ ┴ └───┘
601 subtype_congr_right $
id └─────────────────┘
src └─────────────────┘
typ └─────────────────┘
602 assume x,
id ┴
typ ┴
603 ⟨and.right, λ h₁, ⟨h h₁, h₁⟩⟩
id └───────┘ └┘ ┴ └┘ └┘
src └───────┘
typ └───────┘ └┘ ┴ └┘ └┘
604
605 /-- If a proposition holds for all elements, then the subtype is
606 equivalent to the original type. -/
607 def subtype_univ_equiv {α : Type u} {p : α → Prop} (h : ∀ x, p x) :
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
608 subtype p ≃ α :=
id └─────┘ ┴ ┴ ┴
src └─────┘ ┴
typ └─────┘ ┴ ┴ ┴
doc ┴
609 ⟨λ x, x, λ x, ⟨x, h x⟩, λ x, subtype.eq rfl, λ x, rfl⟩
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ └─┘ ┴ └─┘
src └────────┘ └─┘ └─┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ └─┘ ┴ └─┘
610
611 /-- A subtype of a sigma-type is a sigma-type over a subtype. -/
612 def subtype_sigma_equiv {α : Type u} (p : α → Type v) (q : α → Prop) :
id ┴ ┴
typ ┴ ┴
613 { y : sigma p // q y.1 } ≃ Σ(x : subtype q), p x.1 :=
id ┴ └───┘ ┴ ┴ ┴┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴┴
src ┴ └───┘ ┴ ┴ ┴ └─────┘ ┴ ┴
typ ┴ └───┘ ┴ ┴ ┴┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴┴
doc ┴
614 ⟨λ x, ⟨⟨x.1.1, x.2⟩, x.1.2⟩,
id ┴ ┴┴ ┴ ┴┴ ┴┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴┴ ┴┴ ┴
615 λ x, ⟨⟨x.1.1, x.2⟩, x.1.2⟩,
id ┴ ┴┴ ┴ ┴┴ ┴┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴┴ ┴┴ ┴
616 λ ⟨⟨x, h⟩, y⟩, rfl,
id ┴ └─┘
src └─┘
typ ┴ └─┘
617 λ ⟨⟨x, y⟩, h⟩, rfl⟩
id ┴ └─┘
src └─┘
typ ┴ └─┘
618
619 /-- A sigma type over a subtype is equivalent to the sigma set over the original type,
620 if the fiber is empty outside of the subset -/
621 def sigma_subtype_equiv_of_subset {α : Type u} (p : α → Type v) (q : α → Prop)
id ┴ ┴
typ ┴ ┴
622 (h : ∀ x, p x → q x) :
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
623 (Σ x : subtype q, p x) ≃ Σ x : α, p x :=
id ┴ └─────┘ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src ┴ └─────┘ ┴ ┴ ┴ ┴
typ ┴ └─────┘ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
doc ┴
624 (subtype_sigma_equiv p q).symm.trans $ subtype_univ_equiv $ λ x, h x.1 x.2
id └─────────────────┘ ┴ ┴ └──┘ └───┘ └────────────────┘ ┴ ┴ ┴┴ ┴┴
src └─────────────────┘ └──┘ └───┘ └────────────────┘ ┴ ┴
typ └─────────────────┘ ┴ ┴ └──┘ └───┘ └────────────────┘ ┴ ┴ ┴┴ ┴┴
doc └─────────────────┘ └────────────────┘
625
626 def sigma_subtype_preimage_equiv {α : Type u} {β : Type v} (f : α → β) (p : β → Prop)
id ┴ ┴ ┴
typ ┴ ┴ ┴
627 (h : ∀ x, p (f x)) :
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
628 (Σ y : subtype p, {x : α // f x = y}) ≃ α :=
id ┴ └─────┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └─────┘ ┴ ┴ ┴ ┴
typ ┴ └─────┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
629 calc _ ≃ Σ y : β, {x : α // f x = y} : sigma_subtype_equiv_of_subset _ p (λ y ⟨x, h'⟩, h' ▸ h x)
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────────────────────────┘ ┴ ┴ ┴┴ └┘ ┴ ┴
src ┴ ┴ ┴ ┴ └───────────────────────────┘ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────────────────────────┘ ┴ ┴ ┴┴ └┘ ┴ ┴
doc └───────────────────────────┘
630 ... ≃ α : sigma_preimage_equiv f
id ┴ └──────────────────┘ ┴
src └──────────────────┘
typ ┴ └──────────────────┘ ┴
631
632 def sigma_subtype_preimage_equiv_subtype {α : Type u} {β : Type v} (f : α → β)
id ┴ ┴
typ ┴ ┴
633 {p : α → Prop} {q : β → Prop} (h : ∀ x, p x ↔ q (f x)) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
634 (Σ y : subtype q, {x : α // f x = y}) ≃ subtype p :=
id ┴ └─────┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
src ┴ └─────┘ ┴ ┴ ┴ ┴ └─────┘
typ ┴ └─────┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
doc ┴
635 calc (Σ y : subtype q, {x : α // f x = y}) ≃
id ┴ └─────┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └─────┘ ┴ ┴ ┴
typ ┴ └─────┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
636 Σ y : subtype q, {x : subtype p // subtype.mk (f x) ((h x).1 x.2) = y} :
id ┴ └─────┘ ┴┴ ┴ └─────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src ┴ └─────┘ ┴ ┴ └─────┘ └────────┘ ┴ ┴ ┴
typ ┴ └─────┘ ┴┴ ┴ └─────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
637 begin
st └─────
638 apply sigma_congr_right,
id └───────────────┘
src └────┘└───────────────┘
typ └────┘└───────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────────────┘└─
639 assume y,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───────────┘└─
640 symmetry,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
st ───────────┘└─
641 refine (subtype_subtype_equiv_subtype_exists _ _).trans (subtype_congr_right _),
id └──────────────────────────────────┘ └─────────────────┘
src └─────┘ └──────────────────────────────────┘└──────────┘ └─────────────────┘└─┘
typ └─────┘ └──────────────────────────────────┘└──────────┘ └─────────────────┘└─┘
doc └─────┘ └──────────┘ └─┘
txt └─────┘ └──────────┘ └─┘
par └─────┘ └──────────┘ └─┘
pid ┴ └──────────┘ └─┘
st ──────────────────────────────────────────────────────────────────────────────────┘└─
642 assume x,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───────────┘└─
643 exact ⟨λ ⟨hp, h'⟩, congr_arg subtype.val h', λ h', ⟨(h x).2 (h'.symm ▸ y.2), subtype.eq h'⟩⟩
id └┘ └───────┘ └─────────┘ ┴ ┴ └───┘ ┴ ┴ └────────┘
src └────┘ └┘ └┘ └─┘└───────┘┴└─────────┘┴ └┘ └───┘ ┴ └──┘ └───┘┴┴┴ └───┘└────────┘┴ └──
typ └────┘ └┘ └┘└┘└─┘└───────┘┴└─────────┘┴ └┘ └───┘ ┴┴┴└──┘ └───┘┴┴┴┴└───┘└────────┘┴ └──
doc └────┘ └┘ └┘ └─┘ ┴ ┴ └┘ └───┘ ┴ └──┘ ┴ ┴ └───┘ ┴ └──
txt └────┘ └┘ └┘ └─┘ ┴ ┴ └┘ └───┘ ┴ └──┘ ┴ ┴ └───┘ ┴ └──
par └────┘ └┘ └┘ └─┘ ┴ ┴ └┘ └───┘ ┴ └──┘ ┴ ┴ └───┘ ┴ └──
pid ┴ └┘ └┘ └─┘ ┴ ┴ └┘ └───┘ ┴ └──┘ ┴ ┴ └───┘ ┴ └┘└
st ─────────────────────────────────────────────────────────────────────────────────────────────────
644 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
645
646 ... ≃ subtype p : sigma_preimage_equiv (λ x : subtype p, (⟨f x, (h x).1 x.property⟩ : subtype q))
id └─────┘ ┴ └──────────────────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───────┘ └─────┘ ┴
src └─────┘ └──────────────────┘ └─────┘ ┴ └───────┘ └─────┘
typ └─────┘ ┴ └──────────────────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───────┘ └─────┘ ┴
647
648 def pi_equiv_subtype_sigma (ι : Type*) (π : ι → Type*) :
id ┴
typ ┴
649 (Πi, π i) ≃ {f : ι → Σi, π i | ∀i, (f i).1 = i } :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
650 ⟨ λf, ⟨λi, ⟨i, f i⟩, assume i, rfl⟩, λf i, begin rw ← f.2 i, exact (f.1 i).2 end,
id ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ └───┘ └─┘ └────┘ └─┘ └──┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └───┘┴└─┘┴ └────┘ ┴└─┘┴└──┘
doc └───┘ └─┘ └────┘ └─┘ └──┘
txt └───┘ └─┘ └────┘ └─┘ └──┘
par └───┘ └─┘ └────┘ └─┘ └──┘
pid └─┘ └─┘ ┴ └─┘ ┴└─┘
st └──────────────┘└────────────────┘└─┘
651 assume f, funext $ assume i, rfl,
id ┴ └────┘ ┴ └─┘
src └────┘ └─┘
typ ┴ └────┘ ┴ └─┘
652 assume ⟨f, hf⟩, subtype.eq $ funext $ assume i, sigma.eq (hf i).symm $
id ┴ └┘ └────────┘ └────┘ ┴ └──────┘ ┴ └──┘
src └────────┘ └────┘ └──────┘ └──┘
typ ┴ └┘ └────────┘ └────┘ ┴ └──────┘ ┴ └──┘
653 eq_of_heq $ rec_heq_of_heq _ $ rec_heq_of_heq _ $ heq.refl _⟩
id └───────┘ └────────────┘ └────────────┘ └──────┘
src └───────┘ └────────────┘ └────────────┘ └──────┘
typ └───────┘ └────────────┘ └────────────┘ └──────┘
654
655 def subtype_pi_equiv_pi {α : Sort u} {β : α → Sort v} {p : Πa, β a → Prop} :
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
656 {f : Πa, β a // ∀a, p a (f a) } ≃ Πa, { b : β a // p a b } :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
657 ⟨λf a, ⟨f.1 a, f.2 a⟩, λf, ⟨λa, (f a).1, λa, (f a).2⟩,
id ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
658 by { rintro ⟨f, h⟩, refl },
src └───────────┘ └───┘
typ └───────────┘ └───┘
doc └───────────┘ └───┘
txt └───────────┘ └───┘
par └───────────┘ └───┘
pid └─────┘ ┴
st └──────────────┘└─────┘└┘
659 by { rintro f, funext a, exact subtype.eq' rfl }⟩
id └─────────┘ └─┘
src └──────┘ └──────┘ └────┘└─────────┘┴└─┘┴
typ └──────┘ └──────┘ └────┘└─────────┘┴└─┘┴
doc └──────┘ └──────┘ └────┘ ┴ ┴
txt └──────┘ └──────┘ └────┘ ┴ ┴
par └──────┘ └──────┘ └────┘ ┴ ┴
pid └┘ └┘ ┴ ┴ ┴
st └─────────┘└────────┘└──────────────────────┘└┘
660
661 end
662
663 namespace set
664 open set
665
666 protected def univ (α) : @univ α ≃ α :=
id └──┘ ┴ ┴ ┴
src └──┘ ┴
typ └──┘ ┴ ┴ ┴
doc ┴
667 ⟨subtype.val, λ a, ⟨a, trivial⟩, λ ⟨a, _⟩, rfl, λ a, rfl⟩
id └─────────┘ ┴ ┴ └─────┘ ┴ └─┘ ┴ └─┘
src └─────────┘ └─────┘ └─┘ └─┘
typ └─────────┘ ┴ ┴ └─────┘ ┴ └─┘ ┴ └─┘
668
669 @[simp] lemma univ_apply {α : Type u} (x : @univ α) :
id └──┘ ┴
src └──┘
typ └──┘ ┴
doc └──┘
670 equiv.set.univ α x = x := rfl
id └────────────┘ ┴ ┴ ┴ ┴ └─┘
src └────────────┘ ┴ └─┘
typ └────────────┘ ┴ ┴ ┴ ┴ └─┘
671
672 @[simp] lemma univ_symm_apply {α : Type u} (x : α) :
id ┴
typ ┴
doc └──┘
673 (equiv.set.univ α).symm x = ⟨x, trivial⟩ := rfl
id └────────────┘ ┴ └──┘ ┴ ┴ ┴ └─────┘ └─┘
src └────────────┘ └──┘ ┴ └─────┘ └─┘
typ └────────────┘ ┴ └──┘ ┴ ┴ ┴ └─────┘ └─┘
674
675 protected def empty (α) : (∅ : set α) ≃ empty :=
id ┴ └─┘ ┴ ┴ └───┘
src ┴ └─┘ ┴ └───┘
typ ┴ └─┘ ┴ ┴ └───┘
doc ┴
676 equiv_empty $ λ ⟨x, h⟩, not_mem_empty x h
id └─────────┘ ┴┴ ┴ └───────────┘
src └─────────┘ └───────────┘
typ └─────────┘ ┴┴ ┴ └───────────┘
677
678 protected def pempty (α) : (∅ : set α) ≃ pempty :=
id ┴ └─┘ ┴ ┴ └────┘
src ┴ └─┘ ┴ └────┘
typ ┴ └─┘ ┴ ┴ └────┘
doc ┴ └────┘
679 equiv_pempty $ λ ⟨x, h⟩, not_mem_empty x h
id └──────────┘ ┴┴ ┴ └───────────┘
src └──────────┘ └───────────┘
typ └──────────┘ ┴┴ ┴ └───────────┘
680
681 protected def union' {α} {s t : set α}
id └─┘ ┴
src └─┘
typ └─┘ ┴
682 (p : α → Prop) [decidable_pred p]
id ┴ └────────────┘ ┴
src └────────────┘
typ ┴ └────────────┘ ┴
683 (hs : ∀ x ∈ s, p x)
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
684 (ht : ∀ x ∈ t, ¬ p x) : (s ∪ t : set α) ≃ s ⊕ t :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └─┘ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
doc ┴
685 { to_fun := λ x, if hp : p x.1
id ┴ └┘ ┴ ┴┴
src └┘ ┴
typ ┴ └┘ ┴ ┴┴
686 then sum.inl ⟨_, x.2.resolve_right (λ xt, ht _ xt hp)⟩
id └─────┘ ┴┴ └───────────┘ └┘ └┘ └┘ └┘
src └─────┘ ┴ └───────────┘
typ └─────┘ ┴┴ └───────────┘ └┘ └┘ └┘ └┘
687 else sum.inr ⟨_, x.2.resolve_left (λ xs, hp (hs _ xs))⟩,
id └─────┘ ┴┴ └──────────┘ └┘ └┘ └┘ └┘
src └─────┘ ┴ └──────────┘
typ └─────┘ ┴┴ └──────────┘ └┘ └┘ └┘ └┘
688 inv_fun := λ o, match o with
id ┴ ┴
typ ┴ ┴
689 | (sum.inl x) := ⟨x.1, or.inl x.2⟩
id └─────┘ ┴ ┴ └────┘ ┴
src └─────┘ ┴ └────┘ ┴
typ └─────┘ ┴ ┴ └────┘ ┴
690 | (sum.inr x) := ⟨x.1, or.inr x.2⟩
id └─────┘ ┴ ┴ └────┘ ┴
src └─────┘ ┴ └────┘ ┴
typ └─────┘ ┴ ┴ └────┘ ┴
691 end,
692 left_inv := λ ⟨x, h'⟩, by by_cases p x; simp [union'._match_1, h]; congr,
id ┴ ┴ ┴ └─────────────┘ ┴
src └───────┘ ┴ └────┘ └┘ ┴ └───┘
typ ┴ └───────┘┴┴┴ └────┘└─────────────┘└┘┴┴ └───┘
doc └───────┘ ┴ └────┘ └┘ ┴
txt └───────┘ ┴ └────┘ └┘ ┴ └───┘
par └───────┘ ┴ └────┘ └┘ ┴ └───┘
pid ┴ ┴ ┴┴ └┘ ┴
st └─────────────────────────────────────────────┘
693 right_inv := λ o, begin
id ┴
typ ┴
st └─────
694 rcases o with ⟨x, h⟩ | ⟨x, h⟩;
id ┴
src └─────┘ └───────────────────┘
typ └─────┘┴└───────────────────┘
doc └─────┘ └───────────────────┘
txt └─────┘ └───────────────────┘
par └─────┘ └───────────────────┘
pid ┴ └───────────────────┘
st ───────────────────────────────────
695 dsimp [union'._match_1];
id └─────────────┘
src └─────┘ ┴
typ └─────┘└─────────────┘┴
doc └─────┘ ┴
txt └─────┘ ┴
par └─────┘ ┴
pid ┴┴ ┴
st ─────────────────────────────
696 [simp [hs _ h], simp [ht _ h]]
id ┴ └┘ ┴ └┘ ┴
src ┴└────┘ └─┘ ┴ └────┘ └─┘ ┴
typ ┴└────┘└┘└─┘┴┴ └────┘└┘└─┘┴┴
doc └────┘ └─┘ ┴ └────┘ └─┘ ┴
txt └────┘ └─┘ ┴ └────┘ └─┘ ┴
par └────┘ └─┘ ┴ └────┘ └─┘ ┴
pid ┴┴ └─┘ ┴ ┴┴ └─┘ ┴
st ─────────────────────────────────┘└
697 end }
st ────┘
698
699 protected def union {α} {s t : set α} [decidable_pred s] (H : s ∩ t = ∅) :
id └─┘ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ └────────────┘ ┴ ┴ ┴
typ └─┘ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
700 (s ∪ t : set α) ≃ s ⊕ t :=
id ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
src ┴ └─┘ ┴ ┴
typ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
doc ┴
701 set.union' s (λ _, id) (λ x xt xs, subset_empty_iff.2 H ⟨xs, xt⟩)
id └────────┘ ┴ ┴ └┘ ┴ └┘ └┘ └──────────────┘┴ ┴ └┘ └┘
src └────────┘ └┘ └──────────────┘┴
typ └────────┘ ┴ ┴ └┘ ┴ └┘ └┘ └──────────────┘┴ ┴ └┘ └┘
702
703 lemma union_apply_left {α} {s t : set α} [decidable_pred s] (H : s ∩ t = ∅)
id └─┘ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ └────────────┘ ┴ ┴ ┴
typ └─┘ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
704 {a : (s ∪ t : set α)} (ha : ↑a ∈ s) : equiv.set.union H a = sum.inl ⟨a, ha⟩ :=
id ┴ ┴ ┴ └─┘ ┴ ┴┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴ └─────┘ ┴ └┘
src ┴ └─┘ ┴ ┴ └─────────────┘ ┴ └─────┘
typ ┴ ┴ ┴ └─┘ ┴ ┴┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴ └─────┘ ┴ └┘
705 dif_pos ha
id └─────┘ └┘
src └─────┘
typ └─────┘ └┘
706
707 lemma union_apply_right {α} {s t : set α} [decidable_pred s] (H : s ∩ t = ∅)
id └─┘ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ └────────────┘ ┴ ┴ ┴
typ └─┘ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
708 {a : (s ∪ t : set α)} (ha : ↑a ∈ t) : equiv.set.union H a = sum.inr ⟨a, ha⟩ :=
id ┴ ┴ ┴ └─┘ ┴ ┴┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴ └─────┘ ┴ └┘
src ┴ └─┘ ┴ ┴ └─────────────┘ ┴ └─────┘
typ ┴ ┴ ┴ └─┘ ┴ ┴┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴ └─────┘ ┴ └┘
709 dif_neg (show ↑a ∉ s, by finish [set.ext_iff])
id └─────┘ ┴┴ ┴ ┴ └─────────┘
src └─────┘ ┴ ┴ └──────┘└─────────┘┴
typ └─────┘ ┴┴ ┴ ┴ └──────┘└─────────┘┴
doc └──────┘ ┴
txt └──────┘ ┴
par └──────┘ ┴
pid └┘ ┴
st └───────────────────┘
710
711 protected def singleton {α} (a : α) : ({a} : set α) ≃ punit.{u} :=
id ┴ ┴┴ └─┘ ┴ ┴ └───┘
src ┴ └─┘ ┴ └───┘
typ ┴ ┴┴ └─┘ ┴ ┴ └───┘
doc ┴
712 ⟨λ _, punit.star, λ _, ⟨a, mem_singleton _⟩,
id ┴ └────────┘ ┴ ┴ └───────────┘
src └────────┘ └───────────┘
typ ┴ └────────┘ ┴ ┴ └───────────┘
713 λ ⟨x, h⟩, by { simp at h, subst x },
id ┴ ┴
src └───────┘ └────┘ ┴
typ ┴ └───────┘ └────┘┴┴
doc └───────┘ └────┘ ┴
txt └───────┘ └────┘ ┴
par └───────┘ └────┘ ┴
pid ┴└──┘ ┴ ┴
st └──────────┘└────────┘└┘
714 λ ⟨⟩, rfl⟩
id ┴ └─┘
src ┴ └─┘
typ ┴ └─┘
715
716 protected def of_eq {α : Type u} {s t : set α} (h : s = t) : s ≃ t :=
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
717 { to_fun := λ x, ⟨x.1, h ▸ x.2⟩,
id ┴ ┴┴ ┴ ┴ ┴┴
src ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴┴
718 inv_fun := λ x, ⟨x.1, h.symm ▸ x.2⟩,
id ┴ ┴┴ ┴└───┘ ┴ ┴┴
src ┴ └───┘ ┴ ┴
typ ┴ ┴┴ ┴└───┘ ┴ ┴┴
719 left_inv := λ _, subtype.eq rfl,
id ┴ └────────┘ └─┘
src └────────┘ └─┘
typ ┴ └────────┘ └─┘
720 right_inv := λ _, subtype.eq rfl }
id ┴ └────────┘ └─┘
src └────────┘ └─┘
typ ┴ └────────┘ └─┘
721
722 @[simp] lemma of_eq_apply {α : Type u} {s t : set α} (h : s = t) (a : s) :
id └─┘ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴
typ └─┘ ┴ ┴ ┴ ┴ ┴
doc └──┘
723 equiv.set.of_eq h a = ⟨a, h ▸ a.2⟩ := rfl
id └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ └─┘
src └─────────────┘ ┴ ┴ ┴ └─┘
typ └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ └─┘
724
725 @[simp] lemma of_eq_symm_apply {α : Type u} {s t : set α} (h : s = t) (a : t) :
id └─┘ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴
typ └─┘ ┴ ┴ ┴ ┴ ┴
doc └──┘
726 (equiv.set.of_eq h).symm a = ⟨a, h.symm ▸ a.2⟩ := rfl
id └─────────────┘ ┴ └──┘ ┴ ┴ ┴ ┴└───┘ ┴ ┴┴ └─┘
src └─────────────┘ └──┘ ┴ └───┘ ┴ ┴ └─┘
typ └─────────────┘ ┴ └──┘ ┴ ┴ ┴ ┴└───┘ ┴ ┴┴ └─┘
727
728 protected def insert {α} {s : set.{u} α} [decidable_pred s] {a : α} (H : a ∉ s) :
id └─┘ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴
src └─┘ └────────────┘ ┴
typ └─┘ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴
729 (insert a s : set α) ≃ s ⊕ punit.{u+1} :=
id └────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └───┘
src └────┘ └─┘ ┴ ┴ └───┘
typ └────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └───┘
doc ┴
730 calc (insert a s : set α) ≃ ↥(s ∪ {a}) : equiv.set.of_eq (by simp)
id └────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴┴ └─────────────┘
src └────┘ └─┘ ┴ ┴ ┴ └─────────────┘ └──┘
typ └────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴┴ └─────────────┘ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
731 ... ≃ s ⊕ ({a} : set α) : equiv.set.union (by finish [set.ext_iff])
id ┴ ┴ ┴┴ └─┘ ┴ └─────────────┘ └─────────┘
src ┴ ┴ └─┘ └─────────────┘ └──────┘└─────────┘┴
typ ┴ ┴ ┴┴ └─┘ ┴ └─────────────┘ └──────┘└─────────┘┴
doc └──────┘ ┴
txt └──────┘ ┴
par └──────┘ ┴
pid └┘ ┴
st └───────────────────┘
732 ... ≃ s ⊕ punit.{u+1} : sum_congr (equiv.refl _) (equiv.set.singleton _)
id ┴ ┴ └───┘ └───────┘ └────────┘ └─────────────────┘
src ┴ └───┘ └───────┘ └────────┘ └─────────────────┘
typ ┴ ┴ └───┘ └───────┘ └────────┘ └─────────────────┘
733
734 protected def sum_compl {α} (s : set α) [decidable_pred s] : s ⊕ (-s : set α) ≃ α :=
id └─┘ ┴ └────────────┘ ┴ ┴ ┴ ┴┴ └─┘ ┴ ┴ ┴
src └─┘ └────────────┘ ┴ ┴ └─┘ ┴
typ └─┘ ┴ └────────────┘ ┴ ┴ ┴ ┴┴ └─┘ ┴ ┴ ┴
doc ┴
735 calc s ⊕ (-s : set α) ≃ ↥(s ∪ -s) : (equiv.set.union (by simp [set.ext_iff])).symm
id ┴ ┴ ┴┴ └─┘ ┴ ┴ ┴ ┴ ┴┴ └─────────────┘ └─────────┘ └──┘
src ┴ ┴ └─┘ ┴ ┴ ┴ └─────────────┘ └────┘└─────────┘┴ └──┘
typ ┴ ┴ ┴┴ └─┘ ┴ ┴ ┴ ┴ ┴┴ └─────────────┘ └────┘└─────────┘┴ └──┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └─────────────────┘
736 ... ≃ @univ α : equiv.set.of_eq (by simp)
id └──┘ ┴ └─────────────┘
src └──┘ └─────────────┘ └──┘
typ └──┘ ┴ └─────────────┘ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
737 ... ≃ α : equiv.set.univ _
id ┴ └────────────┘
src └────────────┘
typ ┴ └────────────┘
738
739 @[simp] lemma sum_compl_apply_inl {α : Type u} (s : set α) [decidable_pred s] (x : s) :
id └─┘ ┴ └────────────┘ ┴ ┴
src └─┘ └────────────┘
typ └─┘ ┴ └────────────┘ ┴ ┴
doc └──┘
740 equiv.set.sum_compl s (sum.inl x) = x := rfl
id └─────────────────┘ ┴ └─────┘ ┴ ┴ ┴ └─┘
src └─────────────────┘ └─────┘ ┴ └─┘
typ └─────────────────┘ ┴ └─────┘ ┴ ┴ ┴ └─┘
741
742 @[simp] lemma sum_compl_apply_inr {α : Type u} (s : set α) [decidable_pred s] (x : -s) :
id └─┘ ┴ └────────────┘ ┴ ┴┴
src └─┘ └────────────┘ ┴
typ └─┘ ┴ └────────────┘ ┴ ┴┴
doc └──┘
743 equiv.set.sum_compl s (sum.inr x) = x := rfl
id └─────────────────┘ ┴ └─────┘ ┴ ┴ ┴ └─┘
src └─────────────────┘ └─────┘ ┴ └─┘
typ └─────────────────┘ ┴ └─────┘ ┴ ┴ ┴ └─┘
744
745 lemma sum_compl_symm_apply_of_mem {α : Type u} {s : set α} [decidable_pred s] {x : α}
id └─┘ ┴ └────────────┘ ┴ ┴
src └─┘ └────────────┘
typ └─┘ ┴ └────────────┘ ┴ ┴
746 (hx : x ∈ s) : (equiv.set.sum_compl s).symm x = sum.inl ⟨x, hx⟩ :=
id ┴ ┴ ┴ └─────────────────┘ ┴ └──┘ ┴ ┴ └─────┘ ┴ └┘
src ┴ └─────────────────┘ └──┘ ┴ └─────┘
typ ┴ ┴ ┴ └─────────────────┘ ┴ └──┘ ┴ ┴ └─────┘ ┴ └┘
747 have ↑(⟨x, or.inl hx⟩ : (s ∪ -s : set α)) ∈ s, from hx,
id ┴ ┴ └────┘ └┘ ┴ ┴ ┴┴ └─┘ ┴ ┴ ┴ └┘
src ┴ └────┘ ┴ ┴ └─┘ ┴
typ ┴ ┴ └────┘ └┘ ┴ ┴ ┴┴ └─┘ ┴ ┴ ┴ └┘
748 by { rw [equiv.set.sum_compl], simpa using set.union_apply_left _ this }
id └─────────────────┘ └──────────────────┘ └──┘
src └──┘└─────────────────┘┴ └──────────┘└──────────────────┘└─┘ ┴
typ └──┘└─────────────────┘┴ └──────────┘└──────────────────┘└─┘└──┘┴
doc └──┘ ┴ └──────────┘ └─┘ ┴
txt └──┘ ┴ └──────────┘ └─┘ ┴
par └──┘ ┴ └──────────┘ └─┘ ┴
pid └┘ ┴ ┴└────┘ └─┘ ┴
st └────────────────────────┘└─────────────────────────────────────────┘└┘
749
750 lemma sum_compl_symm_apply_of_not_mem {α : Type u} {s : set α} [decidable_pred s] {x : α}
id └─┘ ┴ └────────────┘ ┴ ┴
src └─┘ └────────────┘
typ └─┘ ┴ └────────────┘ ┴ ┴
751 (hx : x ∉ s) : (equiv.set.sum_compl s).symm x = sum.inr ⟨x, hx⟩ :=
id ┴ ┴ ┴ └─────────────────┘ ┴ └──┘ ┴ ┴ └─────┘ ┴ └┘
src ┴ └─────────────────┘ └──┘ ┴ └─────┘
typ ┴ ┴ ┴ └─────────────────┘ ┴ └──┘ ┴ ┴ └─────┘ ┴ └┘
752 have ↑(⟨x, or.inr hx⟩ : (s ∪ -s : set α)) ∈ -s, from hx,
id ┴ ┴ └────┘ └┘ ┴ ┴ ┴┴ └─┘ ┴ ┴ ┴┴ └┘
src ┴ └────┘ ┴ ┴ └─┘ ┴ ┴
typ ┴ ┴ └────┘ └┘ ┴ ┴ ┴┴ └─┘ ┴ ┴ ┴┴ └┘
753 by { rw [equiv.set.sum_compl], simpa using set.union_apply_right _ this }
id └─────────────────┘ └───────────────────┘ └──┘
src └──┘└─────────────────┘┴ └──────────┘└───────────────────┘└─┘ ┴
typ └──┘└─────────────────┘┴ └──────────┘└───────────────────┘└─┘└──┘┴
doc └──┘ ┴ └──────────┘ └─┘ ┴
txt └──┘ ┴ └──────────┘ └─┘ ┴
par └──┘ ┴ └──────────┘ └─┘ ┴
pid └┘ ┴ ┴└────┘ └─┘ ┴
st └────────────────────────┘└──────────────────────────────────────────┘└┘
754
755 protected def union_sum_inter {α : Type u} (s t : set α) [decidable_pred s] :
id └─┘ ┴ └────────────┘ ┴
src └─┘ └────────────┘
typ └─┘ ┴ └────────────┘ ┴
756 (s ∪ t : set α) ⊕ (s ∩ t : set α) ≃ s ⊕ t :=
id ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
src ┴ └─┘ ┴ ┴ └─┘ ┴ ┴
typ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
doc ┴
757 calc (s ∪ t : set α) ⊕ (s ∩ t : set α)
id ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
src ┴ └─┘ ┴ ┴ └─┘
typ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
758 ≃ (s ∪ t \ s : set α) ⊕ (s ∩ t : set α) : by rw [union_diff_self]
id ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └─────────────┘
src ┴ ┴ └─┘ ┴ ┴ └─┘ └──┘└─────────────┘└┘
typ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └──┘└─────────────┘└┘
doc └──┘ └┘
txt └──┘ └┘
par └──┘ └┘
pid └┘ ┴┴
st └──────────────────┘┴┴
759 ... ≃ (s ⊕ (t \ s : set α)) ⊕ (s ∩ t : set α) :
id ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
src ┴ ┴ └─┘ ┴ ┴ └─┘
typ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
760 sum_congr (set.union (inter_diff_self _ _)) (equiv.refl _)
id └───────┘ └───────┘ └─────────────┘ └────────┘
src └───────┘ └───────┘ └─────────────┘ └────────┘
typ └───────┘ └───────┘ └─────────────┘ └────────┘
761 ... ≃ s ⊕ (t \ s : set α) ⊕ (s ∩ t : set α) : sum_assoc _ _ _
id ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └───────┘
src ┴ ┴ └─┘ ┴ ┴ └─┘ └───────┘
typ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └───────┘
762 ... ≃ s ⊕ (t \ s ∪ s ∩ t : set α) : sum_congr (equiv.refl _) begin
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └───────┘ └────────┘
src ┴ ┴ ┴ ┴ └─┘ └───────┘ └────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └───────┘ └────────┘
st └─────
763 refine (set.union' (∉ s) _ _).symm,
id └────────┘ ┴ ┴
src └─────┘ └────────┘┴┴└┘ └─────────┘
typ └─────┘ └────────┘┴┴└┘┴└─────────┘
doc └─────┘ ┴ └┘ └─────────┘
txt └─────┘ ┴ └┘ └─────────┘
par └─────┘ ┴ └┘ └─────────┘
pid ┴ ┴ └┘ └────────┘┴
st ─────────────────────────────────────┘└─
764 exacts [λ x hx, hx.2, λ x hx, not_not_intro hx.1]
id └───────────┘
src └──────┘ └─────┘ └──┘ └─────┘└───────────┘┴ └───
typ └──────┘ └─────┘ └──┘ └─────┘└───────────┘┴ └───
doc └──────┘ └─────┘ └──┘ └─────┘ ┴ └───
txt └──────┘ └─────┘ └──┘ └─────┘ ┴ └───
par └──────┘ └─────┘ └──┘ └─────┘ ┴ └───
pid └┘ └─────┘ └──┘ └─────┘ ┴ └─┘└
st ──────────────────────────────────────────────────────
765 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
766 ... ≃ s ⊕ t : by { rw (_ : t \ s ∪ s ∩ t = t), rw [union_comm, inter_comm, inter_union_diff] }
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ └────────┘ └──────────────┘
src ┴ └─┘ └──┘ ┴┴┴ ┴┴┴ ┴┴┴ ┴┴┴ ┴ └──┘└────────┘└┘└────────┘└┘└──────────────┘└┘
typ ┴ ┴ ┴ └─┘ └──┘ ┴┴┴ ┴┴┴┴┴┴┴ ┴┴┴┴┴ └──┘└────────┘└┘└────────┘└┘└──────────────┘└┘
doc └─┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └┘ └┘ └┘
txt └─┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └┘ └┘ └┘
par └─┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └┘ └┘ └┘
pid ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └┘ ┴┴
st └───────────────────────────┘└──────────────┘└──────────┘└────────────────┘┴┴└┘
767
768 protected def prod {α β} (s : set α) (t : set β) :
id └─┘ ┴ └─┘ ┴
src └─┘ └─┘
typ └─┘ ┴ └─┘ ┴
769 s.prod t ≃ s × t :=
id ┴└───┘ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴
typ ┴└───┘ ┴ ┴ ┴ ┴ ┴
doc └───┘ ┴
770 ⟨λp, ⟨⟨p.1.1, p.2.1⟩, ⟨p.1.2, p.2.2⟩⟩,
id ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴
771 λp, ⟨⟨p.1.1, p.2.1⟩, ⟨p.1.2, p.2.2⟩⟩,
id ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴
772 λ ⟨⟨x, y⟩, ⟨h₁, h₂⟩⟩, rfl,
id ┴ └─┘
src └─┘
typ ┴ └─┘
773 λ ⟨⟨x, h₁⟩, ⟨y, h₂⟩⟩, rfl⟩
id ┴ └─┘
src └─┘
typ ┴ └─┘
774
775 protected noncomputable def image_of_inj_on {α β} (f : α → β) (s : set α) (H : inj_on f s) :
id ┴ ┴ └─┘ ┴ └────┘ ┴ ┴
src └─┘ └────┘
typ ┴ ┴ └─┘ ┴ └────┘ ┴ ┴
doc └────┘
776 s ≃ (f '' s) :=
id ┴ ┴ ┴ └┘ ┴
src ┴ └┘
typ ┴ ┴ ┴ └┘ ┴
doc ┴
777 ⟨λ ⟨x, h⟩, ⟨f x, mem_image_of_mem f h⟩,
id ┴┴ ┴ ┴ └──────────────┘ ┴
src └──────────────┘
typ ┴┴ ┴ ┴ └──────────────┘ ┴
778 λ ⟨y, h⟩, ⟨classical.some h, (classical.some_spec h).1⟩,
id ┴ ┴ └────────────┘ └─────────────────┘ ┴
src └────────────┘ └─────────────────┘ ┴
typ ┴ ┴ └────────────┘ └─────────────────┘ ┴
779 λ ⟨x, h⟩, subtype.eq (H (classical.some_spec (mem_image_of_mem f h)).1 h
id ┴ ┴ └────────┘ ┴ └─────────────────┘ └──────────────┘ ┴ ┴
src └────────┘ └─────────────────┘ └──────────────┘ ┴
typ ┴ ┴ └────────┘ ┴ └─────────────────┘ └──────────────┘ ┴ ┴
780 (classical.some_spec (mem_image_of_mem f h)).2),
id └─────────────────┘ └──────────────┘ ┴ ┴
src └─────────────────┘ └──────────────┘ ┴
typ └─────────────────┘ └──────────────┘ ┴ ┴
781 λ ⟨y, h⟩, subtype.eq (classical.some_spec h).2⟩
id ┴ ┴ └────────┘ └─────────────────┘ ┴
src └────────┘ └─────────────────┘ ┴
typ ┴ ┴ └────────┘ └─────────────────┘ ┴
782
783 protected noncomputable def image {α β} (f : α → β) (s : set α) (H : injective f) : s ≃ (f '' s) :=
id ┴ ┴ └─┘ ┴ └───────┘ ┴ ┴ ┴ ┴ └┘ ┴
src └─┘ └───────┘ ┴ └┘
typ ┴ ┴ └─┘ ┴ └───────┘ ┴ ┴ ┴ ┴ └┘ ┴
doc ┴
784 equiv.set.image_of_inj_on f s (λ x y hx hy hxy, H hxy)
id └───────────────────────┘ ┴ ┴ ┴ ┴ └┘ └┘ └─┘ ┴ └─┘
src └───────────────────────┘
typ └───────────────────────┘ ┴ ┴ ┴ ┴ └┘ └┘ └─┘ ┴ └─┘
785
786 @[simp] theorem image_apply {α β} (f : α → β) (s : set α) (H : injective f) (a h) :
id ┴ ┴ └─┘ ┴ └───────┘ ┴
src └─┘ └───────┘
typ ┴ ┴ └─┘ ┴ └───────┘ ┴
doc └──┘
787 set.image f s H ⟨a, h⟩ = ⟨f a, mem_image_of_mem _ h⟩ := rfl
id └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────────────┘ ┴ └─┘
src └───────┘ ┴ └──────────────┘ └─┘
typ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────────────┘ ┴ └─┘
788
789 protected noncomputable def range {α β} (f : α → β) (H : injective f) :
id ┴ ┴ └───────┘ ┴
src └───────┘
typ ┴ ┴ └───────┘ ┴
790 α ≃ range f :=
id ┴ ┴ └───┘ ┴
src ┴ └───┘
typ ┴ ┴ └───┘ ┴
doc ┴ └───┘
791 { to_fun := λ x, ⟨f x, mem_range_self _⟩,
id ┴ ┴ ┴ └────────────┘
src └────────────┘
typ ┴ ┴ ┴ └────────────┘
792 inv_fun := λ x, classical.some x.2,
id ┴ └────────────┘ ┴┴
src └────────────┘ ┴
typ ┴ └────────────┘ ┴┴
793 left_inv := λ x, H (classical.some_spec (show f x ∈ range f, from mem_range_self _)),
id ┴ ┴ └─────────────────┘ ┴ ┴ ┴ └───┘ ┴ └────────────┘
src └─────────────────┘ ┴ └───┘ └────────────┘
typ ┴ ┴ └─────────────────┘ ┴ ┴ ┴ └───┘ ┴ └────────────┘
doc └───┘
794 right_inv := λ x, subtype.eq $ classical.some_spec x.2 }
id ┴ └────────┘ └─────────────────┘ ┴┴
src └────────┘ └─────────────────┘ ┴
typ ┴ └────────┘ └─────────────────┘ ┴┴
795
796 @[simp] theorem range_apply {α β} (f : α → β) (H : injective f) (a) :
id ┴ ┴ └───────┘ ┴
src └───────┘
typ ┴ ┴ └───────┘ ┴
doc └──┘
797 set.range f H a = ⟨f a, set.mem_range_self _⟩ := rfl
id └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────────────┘ └─┘
src └───────┘ ┴ └────────────────┘ └─┘
typ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────────────┘ └─┘
798
799 protected def congr {α β : Type*} (e : α ≃ β) : set α ≃ set β :=
id ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
src ┴ └─┘ ┴ └─┘
typ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
doc ┴ ┴
800 ⟨λ s, e '' s, λ t, e.symm '' t, symm_image_image e, symm_image_image e.symm⟩
id ┴ ┴ └┘ ┴ ┴ ┴└───┘ └┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴└───┘
src └┘ └───┘ └┘ └──────────────┘ └──────────────┘ └───┘
typ ┴ ┴ └┘ ┴ ┴ ┴└───┘ └┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴└───┘
801
802 protected def sep {α : Type u} (s : set α) (t : α → Prop) :
id └─┘ ┴ ┴
src └─┘
typ └─┘ ┴ ┴
803 ({ x ∈ s | t x } : set α) ≃ { x : s | t x.1 } :=
id ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴┴
src ┴ └─┘ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴┴
doc ┴
804 (equiv.subtype_subtype_equiv_subtype_inter s t).symm
id └───────────────────────────────────────┘ ┴ ┴ └──┘
src └───────────────────────────────────────┘ └──┘
typ └───────────────────────────────────────┘ ┴ ┴ └──┘
805
806 end set
807
808 noncomputable def of_bijective {α β} {f : α → β} (hf : bijective f) : α ≃ β :=
id ┴ ┴ └───────┘ ┴ ┴ ┴ ┴
src └───────┘ ┴
typ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴
doc ┴
809 ⟨f, λ x, classical.some (hf.2 x), λ x, hf.1 (classical.some_spec (hf.2 (f x))),
id ┴ ┴ └────────────┘ └┘┴ ┴ ┴ └┘┴ └─────────────────┘ └┘┴ ┴ ┴
src └────────────┘ ┴ ┴ └─────────────────┘ ┴
typ ┴ ┴ └────────────┘ └┘┴ ┴ ┴ └┘┴ └─────────────────┘ └┘┴ ┴ ┴
810 λ x, classical.some_spec (hf.2 x)⟩
id ┴ └─────────────────┘ └┘┴ ┴
src └─────────────────┘ ┴
typ ┴ └─────────────────┘ └┘┴ ┴
811
812 @[simp] theorem of_bijective_to_fun {α β} {f : α → β} (hf : bijective f) : (of_bijective hf : α → β) = f := rfl
id ┴ ┴ └───────┘ ┴ └──────────┘ └┘ ┴ ┴ ┴ ┴ └─┘
src └───────┘ └──────────┘ ┴ └─┘
typ ┴ ┴ └───────┘ ┴ └──────────┘ └┘ ┴ ┴ ┴ ┴ └─┘
doc └──┘
813
814 def subtype_quotient_equiv_quotient_subtype (p₁ : α → Prop) [s₁ : setoid α]
id ┴ └────┘ ┴
src └────┘
typ ┴ └────┘ ┴
815 [s₂ : setoid (subtype p₁)] (p₂ : quotient s₁ → Prop) (hp₂ : ∀ a, p₁ a ↔ p₂ ⟦a⟧)
id └────┘ └─────┘ └┘ └──────┘ └┘ ┴ └┘ ┴ ┴ └┘ ┴┴┴
src └────┘ └─────┘ └──────┘ ┴ ┴ ┴
typ └────┘ └─────┘ └┘ └──────┘ └┘ ┴ └┘ ┴ ┴ └┘ ┴┴┴
816 (h : ∀ x y : subtype p₁, @setoid.r _ s₂ x y ↔ (x : α) ≈ y) :
id └─────┘ └┘ └──────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ └──────┘ ┴ ┴
typ └─────┘ └┘ └──────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
817 {x // p₂ x} ≃ quotient s₂ :=
id ┴┴ └┘ ┴ ┴ └──────┘ └┘
src ┴ ┴ └──────┘
typ ┴┴ └┘ ┴ ┴ └──────┘ └┘
doc ┴
818 { to_fun := λ a, quotient.hrec_on a.1 (λ a h, ⟦⟨a, (hp₂ _).2 h⟩⟧)
id ┴ └──────────────┘ ┴┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
src └──────────────┘ ┴ ┴ ┴ ┴
typ ┴ └──────────────┘ ┴┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
819 (λ a b hab, hfunext (by rw quotient.sound hab)
id ┴ ┴ └─┘ └─────┘ └────────────┘ └─┘
src └─────┘ └─┘└────────────┘┴
typ ┴ ┴ └─┘ └─────┘ └─┘└────────────┘┴└─┘
doc └─┘ ┴
txt └─┘ ┴
par └─┘ ┴
pid ┴ ┴
st └────────────────────┘
820 (λ h₁ h₂ _, heq_of_eq (quotient.sound ((h _ _).2 hab)))) a.2,
id └┘ └┘ ┴ └───────┘ └────────────┘ ┴ ┴ └─┘ ┴┴
src └───────┘ └────────────┘ ┴ ┴
typ └┘ └┘ ┴ └───────┘ └────────────┘ ┴ ┴ └─┘ ┴┴
821 inv_fun := λ a, quotient.lift_on a (λ a, (⟨⟦a.1⟧, (hp₂ _).1 a.2⟩ : {x // p₂ x}))
id ┴ └──────────────┘ ┴ ┴ ┴┴┴ ┴ └─┘ ┴ ┴┴ ┴┴ └┘ ┴
src └──────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └──────────────┘ ┴ ┴ ┴┴┴ ┴ └─┘ ┴ ┴┴ ┴┴ └┘ ┴
822 (λ a b hab, subtype.eq' (quotient.sound ((h _ _).1 hab))),
id ┴ ┴ └─┘ └─────────┘ └────────────┘ ┴ ┴ └─┘
src └─────────┘ └────────────┘ ┴
typ ┴ ┴ └─┘ └─────────┘ └────────────┘ ┴ ┴ └─┘
823 left_inv := λ ⟨a, ha⟩, quotient.induction_on a (λ a ha, rfl) ha,
id ┴┴ └┘ └───────────────────┘ ┴ └┘ └─┘
src └───────────────────┘ └─┘
typ ┴┴ └┘ └───────────────────┘ ┴ └┘ └─┘
824 right_inv := λ a, quotient.induction_on a (λ ⟨a, ha⟩, rfl) }
id ┴ └───────────────────┘ ┴ ┴ └─┘
src └───────────────────┘ └─┘
typ ┴ └───────────────────┘ ┴ ┴ └─┘
825
826 section swap
827 variable [decidable_eq α]
id └──────────┘
src └──────────┘
typ └──────────┘
828 open decidable
829
830 def swap_core (a b r : α) : α :=
id ┴ ┴
typ ┴ ┴
831 if r = a then b
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
832 else if r = b then a
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
833 else r
id ┴
typ ┴
834
835 theorem swap_core_self (r a : α) : swap_core a a r = r :=
id ┴ └───────┘ ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴
typ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴
836 by { unfold swap_core, split_ifs; cc }
src └──────────────┘ └───────┘ └─┘
typ └──────────────┘ └───────┘ └─┘
doc └──────────────┘ └───────┘ └─┘
txt └──────────────┘ └───────┘ └─┘
par └──────────────┘ └───────┘ └─┘
pid └────────┘ ┴
st └─────────────────┘└──────────────┘└┘
837
838 theorem swap_core_swap_core (r a b : α) : swap_core a b (swap_core a b r) = r :=
id ┴ └───────┘ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴
src └───────┘ └───────┘ ┴
typ ┴ └───────┘ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴
839 by { unfold swap_core, split_ifs; cc }
src └──────────────┘ └───────┘ └─┘
typ └──────────────┘ └───────┘ └─┘
doc └──────────────┘ └───────┘ └─┘
txt └──────────────┘ └───────┘ └─┘
par └──────────────┘ └───────┘ └─┘
pid └────────┘ ┴
st └─────────────────┘└──────────────┘└┘
840
841 theorem swap_core_comm (r a b : α) : swap_core a b r = swap_core b a r :=
id ┴ └───────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴
src └───────┘ ┴ └───────┘
typ ┴ └───────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴
842 by { unfold swap_core, split_ifs; cc }
src └──────────────┘ └───────┘ └─┘
typ └──────────────┘ └───────┘ └─┘
doc └──────────────┘ └───────┘ └─┘
txt └──────────────┘ └───────┘ └─┘
par └──────────────┘ └───────┘ └─┘
pid └────────┘ ┴
st └─────────────────┘└──────────────┘└┘
843
844 /-- `swap a b` is the permutation that swaps `a` and `b` and
845 leaves other values as is. -/
846 def swap (a b : α) : perm α :=
id ┴ └──┘ ┴
src └──┘
typ ┴ └──┘ ┴
doc └──┘
847 ⟨swap_core a b, swap_core a b, λr, swap_core_swap_core r a b, λr, swap_core_swap_core r a b⟩
id └───────┘ ┴ ┴ └───────┘ ┴ ┴ ┴ └─────────────────┘ ┴ ┴ ┴ ┴ └─────────────────┘ ┴ ┴ ┴
src └───────┘ └───────┘ └─────────────────┘ └─────────────────┘
typ └───────┘ ┴ ┴ └───────┘ ┴ ┴ ┴ └─────────────────┘ ┴ ┴ ┴ ┴ └─────────────────┘ ┴ ┴ ┴
848
849 theorem swap_self (a : α) : swap a a = equiv.refl _ :=
id ┴ └──┘ ┴ ┴ ┴ └────────┘
src └──┘ ┴ └────────┘
typ ┴ └──┘ ┴ ┴ ┴ └────────┘
doc └──┘
850 eq_of_to_fun_eq $ funext $ λ r, swap_core_self r a
id └─────────────┘ └────┘ ┴ └────────────┘ ┴ ┴
src └─────────────┘ └────┘ └────────────┘
typ └─────────────┘ └────┘ ┴ └────────────┘ ┴ ┴
851
852 theorem swap_comm (a b : α) : swap a b = swap b a :=
id ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴
src └──┘ ┴ └──┘
typ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴
doc └──┘ └──┘
853 eq_of_to_fun_eq $ funext $ λ r, swap_core_comm r _ _
id └─────────────┘ └────┘ ┴ └────────────┘ ┴
src └─────────────┘ └────┘ └────────────┘
typ └─────────────┘ └────┘ ┴ └────────────┘ ┴
854
855 theorem swap_apply_def (a b x : α) : swap a b x = if x = a then b else if x = b then a else x :=
id ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴ ┴
typ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
856 rfl
id └─┘
src └─┘
typ └─┘
857
858 @[simp] theorem swap_apply_left (a b : α) : swap a b a = b :=
id ┴ └──┘ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴
typ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
doc └──┘ └──┘
859 if_pos rfl
id └────┘ └─┘
src └────┘ └─┘
typ └────┘ └─┘
860
861 @[simp] theorem swap_apply_right (a b : α) : swap a b b = a :=
id ┴ └──┘ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴
typ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
doc └──┘ └──┘
862 by { by_cases b = a; simp [swap_apply_def, *] }
id ┴ ┴ ┴ └────────────┘
src └───────┘ ┴┴┴ └────┘└────────────┘└───┘
typ └───────┘┴┴┴┴┴ └────┘└────────────┘└───┘
doc └───────┘ ┴ ┴ └────┘ └───┘
txt └───────┘ ┴ ┴ └────┘ └───┘
par └───────┘ ┴ ┴ └────┘ └───┘
pid ┴ ┴ ┴ ┴┴ └──┘┴
st └──────────────────────────────────────────┘└┘
863
864 theorem swap_apply_of_ne_of_ne {a b x : α} : x ≠ a → x ≠ b → swap a b x = x :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └──┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
doc └──┘
865 by simp [swap_apply_def] {contextual := tt}
id └────────────┘ └┘
src └────┘└────────────┘└┘ └────────────┘└┘└─
typ └────┘└────────────┘└┘ └────────────┘└┘└─
doc └────┘ └┘ └────────────┘ └─
txt └────┘ └┘ └────────────┘ └─
par └────┘ └┘ └────────────┘ └─
pid ┴┴ ┴┴ └────────────┘ ┴└
st └─────────────────────────────────────────
866
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
867 @[simp] theorem swap_swap (a b : α) : (swap a b).trans (swap a b) = equiv.refl _ :=
id ┴ └──┘ ┴ ┴ └───┘ └──┘ ┴ ┴ ┴ └────────┘
src └──┘ └───┘ └──┘ ┴ └────────┘
typ ┴ └──┘ ┴ ┴ └───┘ └──┘ ┴ ┴ ┴ └────────┘
doc └──┘ └──┘ └──┘
868 eq_of_to_fun_eq $ funext $ λ x, swap_core_swap_core _ _ _
id └─────────────┘ └────┘ ┴ └─────────────────┘
src └─────────────┘ └────┘ └─────────────────┘
typ └─────────────┘ └────┘ ┴ └─────────────────┘
869
870 theorem swap_comp_apply {a b x : α} (π : perm α) :
id ┴ └──┘ ┴
src └──┘
typ ┴ └──┘ ┴
doc └──┘
871 π.trans (swap a b) x = if π x = a then b else if π x = b then a else π x :=
id ┴└────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────┘ └──┘ ┴ ┴ ┴
typ ┴└────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
872 by { cases π, refl }
id ┴
src └────┘ └───┘
typ └────┘┴ └───┘
doc └────┘ └───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴ ┴
st └────────┘└─────┘└┘
873
874 @[simp] lemma swap_inv {α : Type*} [decidable_eq α] (x y : α) :
id └──────────┘ ┴ ┴
src └──────────┘
typ └──────────┘ ┴ ┴
doc └──┘
875 (swap x y)⁻¹ = swap x y := rfl
id └──┘ ┴ ┴ └┘ ┴ └──┘ ┴ ┴ └─┘
src └──┘ └┘ ┴ └──┘ └─┘
typ └──┘ ┴ ┴ └┘ ┴ └──┘ ┴ ┴ └─┘
doc └──┘ └──┘
876
877 @[simp] lemma symm_trans_swap_trans [decidable_eq β] (a b : α)
id └──────────┘ ┴ ┴
src └──────────┘
typ └──────────┘ ┴ ┴
doc └──┘
878 (e : α ≃ β) : (e.symm.trans (swap a b)).trans e = swap (e a) (e b) :=
id ┴ ┴ ┴ ┴└───┘└────┘ └──┘ ┴ ┴ └───┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
src ┴ └───┘└────┘ └──┘ └───┘ ┴ └──┘
typ ┴ ┴ ┴ ┴└───┘└────┘ └──┘ ┴ ┴ └───┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
doc ┴ └──┘ └──┘
879 equiv.ext _ _ (λ x, begin
id └───────┘ ┴
src └───────┘
typ └───────┘ ┴
st └─────
880 have : ∀ a, e.symm x = a ↔ x = e a :=
id └────┘ ┴ ┴ ┴ ┴
src └─────┘ └┘ ┴└────┘┴ ┴┴┴ ┴┴┴ ┴ ┴ ┴ └───
typ └─────┘ └┘ ┴└────┘┴ ┴┴┴ ┴┴┴┴┴ ┴┴┴ └───
doc └─────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───
txt └─────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───
par └─────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───
pid └───┘└┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───
st ────────────────────────────────────────
881 λ a, by { rw @eq_comm _ (e.symm x), split; intros; simp * at * },
id └─────┘ └────┘ ┴
src ───┘ └──┘ └─┘└─┘ └─────┘└─┘ └────┘┴ ┴└┘└───┘└┘└────┘└┘└──────────┘┴
typ ───┘ └──┘ └─┘└─┘ └─────┘└─┘ └────┘┴┴┴└┘└───┘└┘└────┘└┘└──────────┘┴
doc ───┘ └──┘ └─┘└─┘ └─┘ ┴ ┴└┘└───┘└┘└────┘└┘└──────────┘┴
txt ───┘ └──┘ └─┘└─┘ └─┘ ┴ ┴└┘└───┘└┘└────┘└┘└──────────┘┴
par ───┘ └──┘ └─┘└─┘ └─┘ ┴ ┴└┘└───┘└┘└────┘└┘└──────────┘┴
pid ───┘ └──┘ └────┘ └─┘ ┴ └─────────────────────────────┘
st ──────────┘└─────────────────────────┘└───────────────────────────┘└┘└
882 simp [swap_apply_def, this],
id └────────────┘ └──┘
src └────┘└────────────┘└┘ ┴
typ └────┘└────────────┘└┘└──┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st ────────────────────────────┘└─
883 split_ifs; simp
src └───────┘ └───┘
typ └───────┘ └───┘
doc └───────┘ └───┘
txt └───────┘ └───┘
par └───────┘ └───┘
pid ┴
st ─────────────────┘
884 end)
st └─┘
885
886 @[simp] lemma swap_mul_self {α : Type*} [decidable_eq α] (i j : α) : swap i j * swap i j = 1 :=
id └──────────┘ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
src └──────────┘ └──┘ ┴ └──┘ ┴
typ └──────────┘ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
doc └──┘ └──┘ └──┘
887 equiv.swap_swap i j
id └─────────────┘ ┴ ┴
src └─────────────┘
typ └─────────────┘ ┴ ┴
888
889 @[simp] lemma swap_apply_self {α : Type*} [decidable_eq α] (i j a : α) : swap i j (swap i j a) = a :=
id └──────────┘ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
src └──────────┘ └──┘ └──┘ ┴
typ └──────────┘ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
doc └──┘ └──┘ └──┘
890 by rw [← perm.mul_apply, swap_mul_self, perm.one_apply]
id └────────────┘ └───────────┘ └────────────┘
src └────┘└────────────┘└┘└───────────┘└┘└────────────┘└─
typ └────┘└────────────┘└┘└───────────┘└┘└────────────┘└─
doc └────┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └─
par └────┘ └┘ └┘ └─
pid └──┘ └┘ └┘ ┴└
st └───────────────────┘└─────────────┘└──────────────┘┴└
891
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
892 /-- Augment an equivalence with a prescribed mapping `f a = b` -/
893 def set_value (f : α ≃ β) (a : α) (b : β) : α ≃ β :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴
894 (swap a (f.symm b)).trans f
id └──┘ ┴ ┴└───┘ ┴ └───┘ ┴
src └──┘ └───┘ └───┘
typ └──┘ ┴ ┴└───┘ ┴ └───┘ ┴
doc └──┘
895
896 @[simp] theorem set_value_eq (f : α ≃ β) (a : α) (b : β) : set_value f a b a = b :=
id ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └───────┘ ┴
typ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ ┴ └───────┘
897 by { dsimp [set_value], simp [swap_apply_left] }
id └───────┘ └─────────────┘
src └─────┘└───────┘┴ └────┘└─────────────┘└┘
typ └─────┘└───────┘┴ └────┘└─────────────┘└┘
doc └─────┘└───────┘┴ └────┘ └┘
txt └─────┘ ┴ └────┘ └┘
par └─────┘ ┴ └────┘ └┘
pid ┴┴ ┴ ┴┴ ┴┴
st └──────────────────┘└───────────────────────┘└┘
898
899 end swap
900
901 protected lemma forall_congr {p : α → Prop} {q : β → Prop} (f : α ≃ β)
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
doc ┴
902 (h : ∀{x}, p x ↔ q (f x)) : (∀x, p x) ↔ (∀y, q y) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
903 begin
st └─────
904 split; intros h₂ x,
src └───┘ └─────────┘
typ └───┘ └─────────┘
doc └───┘ └─────────┘
txt └───┘ └─────────┘
par └───┘ └─────────┘
pid └───┘
st ───────────────────┘└─
905 { rw [←f.right_inv x], apply h.mp, apply h₂ },
id └─────────┘ ┴
src └───┘└─────────┘┴ ┴ └────┘ └────┘ ┴
typ └───┘└─────────┘┴┴┴ └────┘ └────┘ ┴
doc └───┘ ┴ ┴ └────┘ └────┘ ┴
txt └───┘ ┴ ┴ └────┘ └────┘ ┴
par └───┘ ┴ ┴ └────┘ └────┘ ┴
pid └─┘ ┴ ┴ ┴ ┴ ┴
st ───┘└────────────────┘└───────────┘└─────────┘└┘└
906 apply h.mpr, apply h₂
src └────┘ └────┘ ┴
typ └────┘ └────┘ ┴
doc └────┘ └────┘ ┴
txt └────┘ └────┘ ┴
par └────┘ └────┘ ┴
pid ┴ ┴ ┴
st ────────────┘└─────────┘
907 end
st └─┘
908
909 end equiv
910
911 instance {α} [subsingleton α] : subsingleton (ulift α) := equiv.ulift.subsingleton
id └──────────┘ ┴ └──────────┘ └───┘ ┴ └─────────┘└───────────┘
src └──────────┘ └──────────┘ └───┘ └─────────┘└───────────┘
typ └──────────┘ ┴ └──────────┘ └───┘ ┴ └─────────┘└───────────┘
doc └───┘
912 instance {α} [subsingleton α] : subsingleton (plift α) := equiv.plift.subsingleton
id └──────────┘ ┴ └──────────┘ └───┘ ┴ └─────────┘└───────────┘
src └──────────┘ └──────────┘ └───┘ └─────────┘└───────────┘
typ └──────────┘ ┴ └──────────┘ └───┘ ┴ └─────────┘└───────────┘
doc └───┘
913
914 instance {α} [decidable_eq α] : decidable_eq (ulift α) := equiv.ulift.decidable_eq
id └──────────┘ ┴ └──────────┘ └───┘ ┴ └─────────┘└───────────┘
src └──────────┘ └──────────┘ └───┘ └─────────┘└───────────┘
typ └──────────┘ ┴ └──────────┘ └───┘ ┴ └─────────┘└───────────┘
doc └───┘
915 instance {α} [decidable_eq α] : decidable_eq (plift α) := equiv.plift.decidable_eq
id └──────────┘ ┴ └──────────┘ └───┘ ┴ └─────────┘└───────────┘
src └──────────┘ └──────────┘ └───┘ └─────────┘└───────────┘
typ └──────────┘ ┴ └──────────┘ └───┘ ┴ └─────────┘└───────────┘
doc └───┘
916
917 def unique_unique_equiv : unique (unique α) ≃ unique α :=
id └────┘ └────┘ ┴ ┴ └────┘ ┴
src └────┘ └────┘ ┴ └────┘
typ └────┘ └────┘ ┴ ┴ └────┘ ┴
doc ┴
918 { to_fun := λ h, h.default,
id ┴ ┴└──────┘
src └──────┘
typ ┴ ┴└──────┘
919 inv_fun := λ h, { default := h, uniq := λ _, subsingleton.elim _ _ },
id ┴ ┴ ┴ └───────────────┘
src └───────────────┘
typ ┴ ┴ ┴ └───────────────┘
920 left_inv := λ _, subsingleton.elim _ _,
id ┴ └───────────────┘
src └───────────────┘
typ ┴ └───────────────┘
921 right_inv := λ _, subsingleton.elim _ _ }
id ┴ └───────────────┘
src └───────────────┘
typ ┴ └───────────────┘
922
923 def equiv_of_unique_of_unique [unique α] [unique β] : α ≃ β :=
id └────┘ ┴ └────┘ ┴ ┴ ┴ ┴
src └────┘ └────┘ ┴
typ └────┘ ┴ └────┘ ┴ ┴ ┴ ┴
doc ┴
924 { to_fun := λ _, default β,
id ┴ └─────┘ ┴
src └─────┘
typ ┴ └─────┘ ┴
925 inv_fun := λ _, default α,
id ┴ └─────┘ ┴
src └─────┘
typ ┴ └─────┘ ┴
926 left_inv := λ _, subsingleton.elim _ _,
id ┴ └───────────────┘
src └───────────────┘
typ ┴ └───────────────┘
927 right_inv := λ _, subsingleton.elim _ _ }
id ┴ └───────────────┘
src └───────────────┘
typ ┴ └───────────────┘
928
929 def equiv_punit_of_unique [unique α] : α ≃ punit.{v} :=
id └────┘ ┴ ┴ ┴ └───┘
src └────┘ ┴ └───┘
typ └────┘ ┴ ┴ ┴ └───┘
doc ┴
930 equiv_of_unique_of_unique
id └───────────────────────┘
src └───────────────────────┘
typ └───────────────────────┘
931
932 namespace quot
933
934 /-- An equivalence `e : α ≃ β` generates an equivalence between quotient spaces,
935 if `ra a₁ a₂ ↔ rb (e a₁) (e a₂). -/
936 protected def congr {ra : α → α → Prop} {rb : β → β → Prop} (e : α ≃ β)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
937 (eq : ∀a₁ a₂, ra a₁ a₂ ↔ rb (e a₁) (e a₂)) :
id └┘ └┘ └┘ └┘ └┘ ┴ └┘ ┴ └┘ ┴ └┘
src ┴
typ └┘ └┘ └┘ └┘ └┘ ┴ └┘ ┴ └┘ ┴ └┘
938 quot ra ≃ quot rb :=
id └──┘ └┘ ┴ └──┘ └┘
src ┴
typ └──┘ └┘ ┴ └──┘ └┘
doc ┴
939 { to_fun := quot.map e (assume a₁ a₂, (eq a₁ a₂).1),
id └──────┘ ┴ └┘ └┘ └┘ └┘ └┘ ┴
src └──────┘ └┘ ┴
typ └──────┘ ┴ └┘ └┘ └┘ └┘ └┘ ┴
doc └──────┘
940 inv_fun := quot.map e.symm
id └──────┘ ┴└───┘
src └──────┘ └───┘
typ └──────┘ ┴└───┘
doc └──────┘
941 (assume b₁ b₂ h,
id └┘ └┘ ┴
typ └┘ └┘ ┴
942 (eq (e.symm b₁) (e.symm b₂)).2
id └┘ ┴└───┘ └┘ ┴└───┘ └┘ ┴
src └┘ └───┘ └───┘ ┴
typ └┘ ┴└───┘ └┘ ┴└───┘ └┘ ┴
943 ((e.apply_symm_apply b₁).symm ▸ (e.apply_symm_apply b₂).symm ▸ h)),
id ┴└───────────────┘ └┘ └──┘ ┴ ┴└───────────────┘ └┘ └──┘ ┴ ┴
src └───────────────┘ └──┘ ┴ └───────────────┘ └──┘ ┴
typ ┴└───────────────┘ └┘ └──┘ ┴ ┴└───────────────┘ └┘ └──┘ ┴ ┴
944 left_inv := by { rintros ⟨a⟩, dunfold quot.map, simp only [equiv.symm_apply_apply] },
id └────────────────────┘
src └─────────┘ └──────────────┘ └─────────┘└────────────────────┘└┘
typ └─────────┘ └──────────────┘ └─────────┘└────────────────────┘└┘
doc └─────────┘ └──────────────┘ └─────────┘ └┘
txt └─────────┘ └──────────────┘ └─────────┘ └┘
par └─────────┘ └──────────────┘ └─────────┘ └┘
pid └──┘ └───────┘ ┴└──┘└┘ ┴┴
st └────────────┘└────────────────┘└───────────────────────────────────┘└┘
945 right_inv := by { rintros ⟨a⟩, dunfold quot.map, simp only [equiv.apply_symm_apply] } }
id └────────────────────┘
src └─────────┘ └──────────────┘ └─────────┘└────────────────────┘└┘
typ └─────────┘ └──────────────┘ └─────────┘└────────────────────┘└┘
doc └─────────┘ └──────────────┘ └─────────┘ └┘
txt └─────────┘ └──────────────┘ └─────────┘ └┘
par └─────────┘ └──────────────┘ └─────────┘ └┘
pid └──┘ └───────┘ ┴└──┘└┘ ┴┴
st └────────────┘└────────────────┘└───────────────────────────────────┘└┘
946
947 /-- Quotients are congruent on equivalences under equality of their relation.
948 An alternative is just to use rewriting with `eq`, but then computational proofs get stuck. -/
949 protected def congr_right {r r' : α → α → Prop} (eq : ∀a₁ a₂, r a₁ a₂ ↔ r' a₁ a₂) :
id ┴ ┴ └┘ └┘ ┴ └┘ └┘ ┴ └┘ └┘ └┘
src ┴
typ ┴ ┴ └┘ └┘ ┴ └┘ └┘ ┴ └┘ └┘ └┘
950 quot r ≃ quot r' :=
id └──┘ ┴ ┴ └──┘ └┘
src ┴
typ └──┘ ┴ ┴ └──┘ └┘
doc ┴
951 quot.congr (equiv.refl α) eq
id └────────┘ └────────┘ ┴ └┘
src └────────┘ └────────┘ └┘
typ └────────┘ └────────┘ ┴ └┘
doc └────────┘
952
953 /-- An equivalence `e : α ≃ β` generates an equivalence between the quotient space of `α`
954 by a relation `ra` and the quotient space of `β` by the image of this relation under `e`. -/
955 protected def congr_left {r : α → α → Prop} (e : α ≃ β) :
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
doc ┴
956 quot r ≃ quot (λ b b', r (e.symm b) (e.symm b')) :=
id └──┘ ┴ ┴ └──┘ ┴ └┘ ┴ ┴└───┘ ┴ ┴└───┘ └┘
src ┴ └───┘ └───┘
typ └──┘ ┴ ┴ └──┘ ┴ └┘ ┴ ┴└───┘ ┴ ┴└───┘ └┘
doc ┴
957 @quot.congr α β r (λ b b', r (e.symm b) (e.symm b')) e (λ a₁ a₂, by simp only [e.symm_apply_apply])
id └────────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴└───┘ ┴ ┴└───┘ └┘ ┴ └┘ └┘
src └────────┘ └───┘ └───┘ └─────────┘ ┴
typ └────────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴└───┘ ┴ ┴└───┘ └┘ ┴ └┘ └┘ └─────────┘└────────────────┘┴
doc └────────┘ └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st └─────────────────────────────┘
958
959 end quot
960
961 namespace quotient
962 /-- An equivalence `e : α ≃ β` generates an equivalence between quotient spaces,
963 if `ra a₁ a₂ ↔ rb (e a₁) (e a₂). -/
964 protected def congr {ra : setoid α} {rb : setoid β} (e : α ≃ β)
id └────┘ ┴ └────┘ ┴ ┴ ┴ ┴
src └────┘ └────┘ ┴
typ └────┘ ┴ └────┘ ┴ ┴ ┴ ┴
doc ┴
965 (eq : ∀a₁ a₂, @setoid.r α ra a₁ a₂ ↔ @setoid.r β rb (e a₁) (e a₂)) :
id └┘ └┘ └──────┘ ┴ └┘ └┘ └┘ ┴ └──────┘ ┴ └┘ ┴ └┘ ┴ └┘
src └──────┘ ┴ └──────┘
typ └┘ └┘ └──────┘ ┴ └┘ └┘ └┘ ┴ └──────┘ ┴ └┘ ┴ └┘ ┴ └┘
966 quotient ra ≃ quotient rb :=
id └──────┘ └┘ ┴ └──────┘ └┘
src └──────┘ ┴ └──────┘
typ └──────┘ └┘ ┴ └──────┘ └┘
doc ┴
967 quot.congr e eq
id └────────┘ ┴ └┘
src └────────┘ └┘
typ └────────┘ ┴ └┘
doc └────────┘
968
969 /-- Quotients are congruent on equivalences under equality of their relation.
970 An alternative is just to use rewriting with `eq`, but then computational proofs get stuck. -/
971 protected def congr_right {r r' : setoid α}
id └────┘ ┴
src └────┘
typ └────┘ ┴
972 (eq : ∀a₁ a₂, @setoid.r α r a₁ a₂ ↔ @setoid.r α r' a₁ a₂) : quotient r ≃ quotient r' :=
id └┘ └┘ └──────┘ ┴ ┴ └┘ └┘ ┴ └──────┘ ┴ └┘ └┘ └┘ └──────┘ ┴ ┴ └──────┘ └┘
src └──────┘ ┴ └──────┘ └──────┘ ┴ └──────┘
typ └┘ └┘ └──────┘ ┴ ┴ └┘ └┘ ┴ └──────┘ ┴ └┘ └┘ └┘ └──────┘ ┴ ┴ └──────┘ └┘
doc ┴
973 quot.congr_right eq
id └──────────────┘ └┘
src └──────────────┘ └┘
typ └──────────────┘ └┘
doc └──────────────┘
974 end quotient